/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ α`REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC

␈↓ α∧␈↓α␈↓ ∧tby R. S. Cartwright and John McCarthy











␈↓ α∧␈↓␈↓ αTPure␈αLisp␈αstyle␈αrecursive␈αfunction␈αprograms␈αare␈αrepresented␈αin␈αa␈αnew␈αway␈αby␈αsentences␈αand
␈↓ α∧␈↓schemata␈α
of␈α
first␈α
order␈α∞logic.␈α
 This␈α
permits␈α
easy␈α
and␈α∞natural␈α
proofs␈α
of␈α
extensional␈α∞properties␈α
of
␈↓ α∧␈↓such␈α∂programs␈α∂and␈α⊂systematizes␈α∂known␈α∂methods␈α∂such␈α⊂as␈α∂␈↓↓recursion␈α∂induction␈↓,␈α⊂␈↓↓subgoal␈α∂induction␈↓,
␈↓ α∧␈↓␈↓↓inductive␈α
assertions␈↓.␈α
 We␈α
discuss␈α
the␈α
metatheorems␈α
justifying␈α
the␈α
representation␈α
and␈α
techniques␈α
for
␈↓ α∧␈↓proving␈αfacts␈αabout␈αspecific␈αprograms.␈α We␈α
also␈αgive␈αa␈αsimpler␈αversion␈αof␈αthe␈α
G␈↓
:␈↓odel-Kleene␈αway
␈↓ α∧␈↓of representing computable functions by first order sentences.

␈↓ α∧␈↓␈↓εThis draft of FIRST[W79,JMC] PUBbed at 13:30 on January 21, 1979.␈↓
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ u2


␈↓ α∧␈↓α1. Introduction and Motivation.

␈↓ α∧␈↓␈↓ αTThis␈αpaper␈αadvances␈αtwo␈αaspects␈αof␈αthe␈αstudy␈αof␈αthe␈αproperties␈αof␈αcomputer␈αprograms␈α-␈αthe
␈↓ α∧␈↓scientifically␈α
motivated␈α
search␈α
for␈α
general␈αtheorems␈α
that␈α
permit␈α
deducing␈α
properties␈α
of␈αprograms
␈↓ α∧␈↓and␈α∩the␈α∩engineering␈α∩problem␈α∩of␈α∩replacing␈α∩debugging␈α∩by␈α∩computer-assisted␈α∩computer-checked
␈↓ α∧␈↓proofs␈α∂that␈α∂programs␈α∞have␈α∂desired␈α∂properties.␈α∞ Both␈α∂tasks␈α∂require␈α∞mathematics,␈α∂but␈α∂the␈α∞second
␈↓ α∧␈↓also␈α
requires␈α
keeping␈α
a␈α
non-mathematical␈α
goal␈αin␈α
mind␈α
-␈α
getting␈α
short␈α
completely␈α
formal␈αproofs
␈↓ α∧␈↓that are easy to write and check by computer.

␈↓ α∧␈↓␈↓ αTCartwright␈α(1976)␈αshows␈αhow␈αa␈αrecursive␈αprogram␈α(as␈αin␈αpure␈αLisp)␈αdefines␈αa␈αfunction␈αin␈αa
␈↓ α∧␈↓first␈α∀order␈α∀theory.␈α∀ The␈α∀function␈α∀satisfies␈α∪a␈α∀␈↓↓functional␈α∀equation␈↓␈α∀trivially␈α∀obtained␈α∀from␈α∪the
␈↓ α∧␈↓program,␈αand␈αif␈αthe␈αprogram␈αalways␈αterminates,␈αthe␈αfunctional␈αequation␈αhas␈αa␈αunique␈αsolution.␈α
 If
␈↓ α∧␈↓the␈αprogram␈αdoes␈αnot␈αalways␈αterminate,␈αthe␈αfunctional␈αequation␈αmay␈αnot␈αfully␈αcharacterize␈αit,␈αand
␈↓ α∧␈↓we␈α⊂supplement␈α⊂the␈α⊂␈↓↓functional␈α∂equation␈↓␈α⊂by␈α⊂a␈α⊂␈↓↓minimization␈α∂schema␈↓␈α⊂or␈α⊂by␈α⊂an␈α⊂associated␈α∂␈↓↓complete
␈↓ α∧␈↓↓recursive␈αprogram␈↓,␈αeither␈αof␈αwhich␈αcompletes␈αthe␈αcharacterization,␈αas␈αis␈αshown␈αin␈α(Cartwright␈αand
␈↓ α∧␈↓McCarthy␈α↔1979).␈α↔ Given␈α_the␈α↔functional␈α↔equation␈α_and␈α↔minimization␈α↔schema,␈α_any␈α↔sentence
␈↓ α∧␈↓involving␈α⊃the␈α⊂function␈α⊃defined␈α⊃by␈α⊂the␈α⊃program␈α⊂can␈α⊃be␈α⊃proved␈α⊂within␈α⊃first␈α⊂order␈α⊃logic␈α⊃to␈α⊂be
␈↓ α∧␈↓equivalent␈α∂to␈α∂a␈α∂sentence␈α∂not␈α∂involving␈α∂the␈α∂function,␈α∂i.e.␈α∂a␈α∂sentence␈α∂in␈α∂the␈α∂data␈α∂domain.␈α∂ Thus
␈↓ α∧␈↓nonexistence␈α
of␈α
a␈α
proof␈α
or␈αdisproof␈α
of␈α
the␈α
total␈α
correctness␈α
of␈αa␈α
program␈α
or␈α
the␈α
equivalence␈αof␈α
two
␈↓ α∧␈↓programs is just a matter of the G␈↓
:␈↓odelian incompleteness and undecideability of the data domain.

␈↓ α∧␈↓␈↓ αTWhile␈α
we␈αshall␈α
prove␈αsome␈α
theoretical␈α
results␈αand␈α
cite␈αothers,␈α
the␈α
main␈αcontent␈α
of␈αthis␈α
paper
␈↓ α∧␈↓is a discussion of the application of these new methods to the verification of recursive programs.

␈↓ α∧␈↓␈↓ αTIt␈α
has␈αbeen␈α
concluded␈αfrom␈α
the␈α
undecideability␈αof␈α
both␈αequivalence␈α
and␈αnon-equivalence␈α
of
␈↓ α∧␈↓abstract␈α⊃recursive␈α⊃program␈α⊃schemata␈α⊃that␈α⊃recursive␈α⊃programs␈α⊃cannot␈α⊃be␈α⊃characterized␈α⊃in␈α⊂first
␈↓ α∧␈↓order␈α⊂logic.␈α⊃ Cooper␈α⊂(1969)␈α⊂showed␈α⊃how␈α⊂to␈α⊂characterize␈α⊃them␈α⊂in␈α⊂second␈α⊃order␈α⊂logic,␈α⊃and␈α⊂that
␈↓ α∧␈↓seemed␈α∂to␈α∞settle␈α∂the␈α∞matter.␈α∂ However,␈α∂these␈α∞results,␈α∂though␈α∞correct,␈α∂are␈α∞misleading,␈α∂and␈α∂it␈α∞now
␈↓ α∧␈↓seems␈α∃likely␈α∃that␈α∃all␈α∃"ordinary"␈α∃␈↓↓extensional␈↓␈α∃assertions␈α∃about␈α∃programs␈α∃will␈α∃be␈α∃provable␈α∀or
␈↓ α∧␈↓disprovable␈αin␈αfirst␈αorder␈αtheories.␈α ␈↓↓Extensional␈↓␈αassertions␈αabout␈αa␈αprogram␈αconcern␈αthe␈αfunctions
␈↓ α∧␈↓computed␈αby␈αthe␈αprogram␈αand␈αnot␈αthe␈αmanner␈αof␈αcomputation.␈α That␈αa␈αmerge␈αsort␈αprogram␈αgives
␈↓ α∧␈↓the␈αsame␈αresult␈αas␈αa␈αbubble␈αsort␈αprogram␈αis␈αan␈αextensional␈αassertion,␈αbut␈αthe␈αfact␈αthat␈αit␈αdoes␈αless
␈↓ α∧␈↓computation is not.

␈↓ α∧␈↓␈↓ αTBesides␈αilluminating␈αthe␈αlogical␈αstructure␈αof␈αcomputer␈αprograms,␈αthese␈αresults␈αhave␈αpractical
␈↓ α∧␈↓significance.␈α∪ First,␈α∀the␈α∪correctness␈α∪of␈α∀a␈α∪computer␈α∪program␈α∀often␈α∪involves␈α∪facts␈α∀about␈α∪other
␈↓ α∧␈↓mathematical␈αdomains,␈α
and␈αthese␈αare␈α
often␈αconveniently␈αexpressed␈α
in␈αfirst␈αorder␈α
logic␈αor␈αin␈α
a␈αset
␈↓ α∧␈↓theory␈αaxiomatized␈α
in␈αfirst␈α
order␈αlogic.␈α
 It␈αhas␈αproved␈α
particularly␈αdifficult␈α
to␈αwork␈α
within␈αlogics
␈↓ α∧␈↓that␈α∃admit␈α∀only␈α∃continuous␈α∀functions␈α∃and␈α∀predicates.␈α∃ Second,␈α∀proof-checking␈α∃and␈α∀theorem
␈↓ α∧␈↓proving␈αprograms␈αhave␈αbeen␈αdeveloped␈αfor␈αfirst␈αorder␈αlogic.␈α Finally,␈αfirst␈αorder␈αlogic␈αis␈αcomplete,
␈↓ α∧␈↓so␈α∞that␈α∞the␈α∂G␈↓
:␈↓odelian␈α∞incompleteness␈α∞of␈α∂any␈α∞theory␈α∞is␈α∞in␈α∂the␈α∞set␈α∞of␈α∂axioms␈α∞and␈α∞can␈α∂be␈α∞reduced
␈↓ α∧␈↓when necessary by adding axioms rather than by changing the logical system.

␈↓ α∧␈↓␈↓ αTWhile␈α↔our␈α↔goal␈α↔is␈α⊗first␈α↔order␈α↔representations␈α↔of␈α⊗recursive␈α↔programs,␈α↔we␈α↔will␈α⊗make
␈↓ α∧␈↓considerable informal use of higher order functionals and predicates.

␈↓ α∧␈↓␈↓ αTWe␈α⊗present␈α↔two␈α⊗methods␈α↔of␈α⊗representing␈α↔recursive␈α⊗programs.␈α↔ The␈α⊗first␈α↔involves␈α⊗a
␈↓ α∧␈↓␈↓↓functional␈α∞equation␈↓␈α∞and␈α∞a␈α∞␈↓↓minimization␈α∞schema␈↓␈α∞for␈α∞each␈α∞program.␈α∞ The␈α∞functional␈α∞equation␈α∞has
␈↓ α∧␈↓the␈αfunction␈αon␈αboth␈αsides␈αof␈αan␈αequality␈αsign␈αand␈αso␈αdefines␈αit␈αimplicitly.␈α However,␈αall␈αvariables
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ u3


␈↓ α∧␈↓are␈α∞universally␈α∞quantified.␈α∞ The␈α∞second␈α∂approach␈α∞defines␈α∞the␈α∞function␈α∞explicitly,␈α∂but␈α∞existential
␈↓ α∧␈↓quantifiers asserting the existence of finite approximations to the function occur in the formula.

␈↓ α∧␈↓␈↓ αTThe␈α∂idea␈α∂of␈α∂the␈α∂first␈α∂order␈α∂functional␈α∂equation␈α∂is␈α∂so␈α∂straightforward,␈α∂that␈α∂one␈α∂wants␈α∞an
␈↓ α∧␈↓explanation␈αof␈αwhy␈αit␈αdidn't␈αarise␈αearlier.␈α The␈αkey␈αdiscovery␈αmay␈αbe␈αthat␈αit␈αis␈αnecessary␈αto␈αhave
␈↓ α∧␈↓two␈αkinds␈αof␈αequality␈α-␈αordinary␈αlogical␈αequality␈αin␈αwhich␈αthe␈αundefined␈αelement␈α␈↓πT␈↓␈αis␈αunequal␈αto
␈↓ α∧␈↓other objects and a "continuous" equality in which such an equality has ␈↓πT␈↓ as value.

␈↓ α∧␈↓␈↓ αTAn␈α
adequate␈α
background␈α
for␈α
this␈α
paper␈α
is␈α
contained␈α
in␈α
(Manna␈α
1974)␈α
and␈α
more␈α
concisely␈α
in
␈↓ α∧␈↓(Manna,␈α∂Ness␈α∞and␈α∂Vuillemin␈α∞1973).␈α∂ The␈α∞connections␈α∂of␈α∞recursive␈α∂programs␈α∞with␈α∂second␈α∞order
␈↓ α∧␈↓logic are given in (Cooper 1969) and (Park 1970).


␈↓ α∧␈↓α2. Recursive Programs.

␈↓ α∧␈↓␈↓ αTWe consider recursive programs like

␈↓ α∧␈↓1)␈↓ αt ␈↓↓n! ← ␈↓αif␈↓↓ n = 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ n . (n - 1)!␈↓

␈↓ α∧␈↓which␈αis␈αthe␈αwell␈αknown␈αrecursive␈αprogram␈αfor␈αthe␈αfactorial␈αfunction.␈α Programs␈αgiven␈αby␈αsets␈αof
␈↓ α∧␈↓mutually function programs will also be considered.

␈↓ α∧␈↓␈↓ αTAnother␈α∂example␈α∂is␈α∂the␈α∂Lisp␈α∂program␈α∂␈↓↓append[u,v]␈↓.␈α∂ In␈α∂this␈α∂paper␈α∂we␈α∂will␈α∂use␈α⊂the␈α∂Lisp
␈↓ α∧␈↓external␈α⊃or␈α⊃publication␈α⊃notation␈α⊃of␈α⊃(McCarthy␈α⊃and␈α⊃Talcott␈α⊃1979),␈α⊃and␈α⊃we␈α⊃will␈α⊃write␈α⊃␈↓↓u*v␈↓␈α⊃for
␈↓ α∧␈↓␈↓↓append[u,v]␈↓.  We then have

␈↓ α∧␈↓2)␈↓ αt ␈↓↓u * v ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓.

␈↓ α∧␈↓Here␈α
we␈α
are␈α
using␈α
␈↓αn␈↓␈α
for␈α
␈↓↓null,␈↓␈α
␈↓αa␈↓␈α
for␈α
␈↓↓car,␈↓␈α
␈↓αd␈↓␈α
for␈α
␈↓↓cdr␈↓␈α
and␈α
an␈α
infixed␈α
.␈α
for␈α
␈↓↓cons.␈↓␈α
We␈α
omit␈αbrackets␈α
for
␈↓ α∧␈↓functions of one argument.  In a more traditional Lisp M-expression notation we would have

␈↓ α∧␈↓␈↓ αT␈↓↓append[u,v] ← ␈↓αif␈↓↓ null[u] ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ cons[car[u], append[cdr[u], v]]␈↓,

␈↓ α∧␈↓and in Maclisp S-expression notation, this would be

␈↓ α∧␈↓␈↓ αT(DEFUN␈αAPPEND␈α(U␈αV)␈α(COND␈α((NULL␈αU)␈αV)␈α(T␈α(CONS␈α(CAR␈αU)␈α(APPEND␈α(CDR
␈↓ α∧␈↓U) V))))).

␈↓ α∧␈↓␈↓ αTOur␈α
objective␈α
is␈α∞to␈α
prove␈α
facts␈α∞about␈α
such␈α
recursively␈α∞defined␈α
functions␈α
by␈α∞regarding␈α
the
␈↓ α∧␈↓recursive␈α
function␈αdefinitions␈α
as␈αsentences␈α
of␈αfirst␈α
order␈αlogic.␈α
 More␈αaccurately,␈α
we␈α
represent␈αthe
␈↓ α∧␈↓recursive␈αfunction␈αdefinitions␈αby␈αvery␈αsimilar␈αsentences␈αof␈αfirst␈αorder␈αlogic.␈α Equations␈α(1)␈αand␈α(2)
␈↓ α∧␈↓are translated into the sentences

␈↓ α∧␈↓3)␈↓ αt ␈↓↓∀n.(n! = IF n = 0 THEN 1 ELSE n ␈↓πx␈↓↓ (n - 1)!)␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓4)␈↓ αt ␈↓↓∀u v.(u * v = IF null u THEN v ELSE ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v])␈↓
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ u4


␈↓ α∧␈↓respectively.␈α⊂ The␈α⊂slight␈α⊂changes␈α∂in␈α⊂notation␈α⊂between␈α⊂the␈α∂programs␈α⊂and␈α⊂logical␈α⊂sentences␈α∂keep
␈↓ α∧␈↓everything␈αlogically␈αcorrect␈α
and␈αwill␈αbe␈αexplained␈α
later.␈α As␈αwill␈αalso␈α
be␈αexplained␈αlater,␈α
we␈αhave
␈↓ α∧␈↓extended␈αfirst␈α
order␈αlogic␈α
to␈αallow␈α
conditional␈αexpressions␈α
as␈αterms.␈α
 This␈αkeeps␈α
the␈αsentences␈α
close
␈↓ α∧␈↓to the programs without affecting the metamathematical properties of first order logic.

␈↓ α∧␈↓␈↓ αTThe␈αsentences␈α(3)␈αand␈α(4)␈αcompletely␈αcharacterize␈αthe␈αfunctions␈αdefined␈αby␈αthe␈αprograms␈α(1)
␈↓ α∧␈↓and␈α⊃(2),␈α∩so␈α⊃proofs␈α∩of␈α⊃the␈α⊃properties␈α∩of␈α⊃these␈α∩functions␈α⊃can␈α⊃be␈α∩deduced␈α⊃from␈α∩these␈α⊃sentences
␈↓ α∧␈↓together␈αwith␈αaxioms␈αcharacterizing␈αthe␈αnatural␈αnumber␈αand␈αLisp␈αdata␈αdomains␈αrespectively.␈α For
␈↓ α∧␈↓example, suppose we wish to prove that * satisfies the equations

␈↓ α∧␈↓5)␈↓ αt ␈↓↓∀v.(␈↓NIL␈↓↓ * v = v)␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓6)␈↓ αt ␈↓↓∀u.(u * ␈↓NIL␈↓↓ = u)␈↓,

␈↓ α∧␈↓i.e.␈α∪NIL␈α∩is␈α∪both␈α∪a␈α∩left␈α∪and␈α∪right␈α∩identity␈α∪for␈α∪the␈α∩*␈α∪operation.␈α∪ (5)␈α∩is␈α∪trivially␈α∪obtained␈α∩by
␈↓ α∧␈↓substituting␈α
NIL␈αfor␈α
␈↓↓u␈↓␈αin␈α
(3)␈α
and␈αusing␈α
the␈αrules␈α
for␈α
evaluating␈αconditional␈α
expressions␈αwhich␈α
will
␈↓ α∧␈↓have␈α∞been␈α∞added␈α∞to␈α∞the␈α∂usual␈α∞rules␈α∞for␈α∞first␈α∞order␈α∂logic.␈α∞ (6)␈α∞expresses␈α∞a␈α∞more␈α∂typical␈α∞program
␈↓ α∧␈↓property in that its proof requires a mathematical induction.

␈↓ α∧␈↓This induction is accomplished by substituting

␈↓ α∧␈↓␈↓ αT␈↓↓␈↓	F␈↓↓(u) ≡ (u = ␈↓NIL␈↓↓)␈↓

␈↓ α∧␈↓in the list induction schema

␈↓ α∧␈↓␈↓ αT␈↓↓␈↓	F␈↓↓(␈↓NIL␈↓↓) ∧ ∀u.(¬null u ∧ ␈↓	F␈↓↓(␈↓αd␈↓↓ u) ⊃ ␈↓	F␈↓↓(u)) ⊃ ∀u.␈↓	F␈↓↓(u)␈↓,

␈↓ α∧␈↓and␈α
using␈α(4),␈α
the␈αaxioms␈α
for␈α
lists,␈αand␈α
the␈αrules␈α
of␈α
inference␈αof␈α
first␈αorder␈α
logic␈α
including␈αthose
␈↓ α∧␈↓for conditional expressions.

␈↓ α∧␈↓␈↓ αTThe␈α
translation␈α
of␈αthe␈α
program␈α
into␈α
a␈αlogical␈α
sentences␈α
would␈α
be␈αtrivial␈α
to␈α
justify␈α
if␈αwe␈α
were
␈↓ α∧␈↓always␈α∂assured␈α∂that␈α⊂the␈α∂program␈α∂terminates␈α∂for␈α⊂all␈α∂sets␈α∂of␈α∂arguments␈α⊂and␈α∂thus␈α∂defines␈α⊂a␈α∂total
␈↓ α∧␈↓function.␈α∞ The␈α∞innovation␈α∞is␈α∞that␈α∞the␈α∞translation␈α∞is␈α∞possible␈α∞even␈α∞without␈α∞that␈α∞guarantee␈α∞at␈α
the
␈↓ α∧␈↓cheap␈α⊃price␈α⊃of␈α⊃extending␈α∩the␈α⊃data␈α⊃domain␈α⊃by␈α∩an␈α⊃undefined␈α⊃element␈α⊃␈↓πT␈↓,␈α∩rewriting␈α⊃recursively
␈↓ α∧␈↓defined␈α⊂predicates␈α⊂as␈α⊂functions,␈α∂having␈α⊂two␈α⊂kinds␈α⊂of␈α∂equality␈α⊂and␈α⊂conditional␈α⊂expression,␈α∂and
␈↓ α∧␈↓providing␈α
each␈αpredicate␈α
with␈α
two␈αforms␈α
-␈αone␈α
a␈α
true␈αpredicate␈α
and␈α
the␈αother␈α
a␈αfunction␈α
imitating
␈↓ α∧␈↓the␈α
predicate.␈α∞ Once␈α
we␈α
have␈α∞done␈α
this,␈α∞proofs␈α
of␈α
termination␈α∞will␈α
take␈α
the␈α∞same␈α
form␈α∞as␈α
other
␈↓ α∧␈↓inductive␈α
proofs.␈α
 Howver,␈α∞additional␈α
formalism␈α
is␈α∞required␈α
to␈α
characterize␈α∞completely␈α
programs
␈↓ α∧␈↓that don't always terminate.

␈↓ α∧␈↓␈↓ αTWe␈αmust␈α
distinguish␈αbetween␈α
a␈αprogram␈α
as␈αa␈α
text␈αand␈α
the␈αpartial␈α
function␈αdefined␈α
by␈αthe
␈↓ α∧␈↓program␈α
when␈α
we␈α
are␈α
want␈α
to␈α
describe␈α
the␈α
dependence␈α
of␈α
the␈α
function␈α
on␈α
the␈α
interpretation␈αof␈α
the
␈↓ α∧␈↓basic␈α
function␈α
and␈α
predicate␈α
symbols.␈α
 However,␈α
we␈α
will␈α
be␈α
working␈α
with␈α
just␈α
one␈α
interpretation␈α
at
␈↓ α∧␈↓a time, so we won't use separate symbols for programs and the functions they determine.

␈↓ α∧␈↓␈↓ αTThe␈α⊂next␈α⊂sections␈α⊃introduce␈α⊂the␈α⊂logical␈α⊃basis␈α⊂of␈α⊂the␈α⊃formalism␈α⊂and␈α⊂axioms␈α⊃and␈α⊂axioms
␈↓ α∧␈↓schemata for Lisp.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ u5


␈↓ α∧␈↓α3. Two Useful Extensions to First Order Logic.

␈↓ α∧␈↓␈↓ αTWe␈α
begin␈α
by␈α
extending␈α
first␈α
order␈α∞logic␈α
to␈α
include␈α
conditional␈α
expressions␈α
and␈α∞first␈α
order
␈↓ α∧␈↓lambda␈αexpressions.␈α Translating␈αrecursive␈αprograms␈αinto␈αlogical␈αsentences␈αcould␈αbe␈αaccomplished
␈↓ α∧␈↓without␈α∪these␈α∪extensions,␈α∪but␈α∪the␈α∪resulting␈α∪sentences␈α∪would␈α∪often␈α∪be␈α∪much␈α∪longer␈α∪than␈α∪the
␈↓ α∧␈↓programs␈α
and␈α
their␈α∞relation␈α
to␈α
the␈α
program␈α∞would␈α
be␈α
obscured.␈α
 Since␈α∞we␈α
are␈α
creating␈α∞tools␈α
for
␈↓ α∧␈↓proving␈αproperties␈αof␈αactual␈αprograms,␈αwe␈αmust␈αface␈αthe␈αfact␈αthat␈αuseful␈αprograms␈αare␈αquite␈αlong
␈↓ α∧␈↓enough␈αas␈αit␈αis.␈α Obscuring␈αtheir␈αcontent␈αin␈αthe␈αcourse␈αof␈αtranslating␈αthem␈αinto␈αlogic␈αmight␈αmake
␈↓ α∧␈↓program proving impractical or at least much more difficult.

␈↓ α∧␈↓␈↓ αTOn␈αthe␈αother␈αhand,␈αwe␈αcannot␈αadd␈αarbitrary␈αprogramming␈αconstructions␈αto␈αfirst␈αorder␈αlogic
␈↓ α∧␈↓without␈α
risking␈α
its␈αuseful␈α
properties␈α
such␈αas␈α
completeness␈α
or␈αeven␈α
consistency.␈α
 Fortunately,␈αthese
␈↓ α∧␈↓are␈αharmless␈αand␈αgenerally␈αuseful␈αextensions.␈α In␈αfact,␈αthey␈αare␈αuseful␈αfor␈αexpressing␈αmathematical
␈↓ α∧␈↓ideas␈α
concisely␈αand␈α
understandably␈αquite␈α
apart␈α
from␈αapplications␈α
to␈αcomputer␈α
science.␈α The␈α
reader
␈↓ α∧␈↓is␈α∞assumed␈α∞to␈α∞know␈α∞about␈α∞first␈α
order␈α∞logic,␈α∞conditional␈α∞expressions␈α∞and␈α∞lambda␈α∞expressions;␈α
we
␈↓ α∧␈↓explain only their connection.

␈↓ α∧␈↓␈↓ αTRemember␈α
that␈αthe␈α
syntax␈αof␈α
first␈αorder␈α
logic␈αis␈α
given␈αin␈α
the␈αform␈α
of␈αinductive␈α
rules␈αfor␈α
the
␈↓ α∧␈↓formation of terms and wffs.  The rule for forming terms is extended as follows:

␈↓ α∧␈↓␈↓ αTIf␈α∞␈↓↓p␈↓␈α
is␈α∞a␈α∞wff␈α
and␈α∞␈↓↓a␈↓␈α
and␈α∞␈↓↓b␈↓␈α∞are␈α
terms,␈α∞then␈α∞␈↓↓IF␈α
p␈α∞THEN␈α
a␈α∞ELSE␈α∞b␈↓␈α
is␈α∞a␈α∞term.␈α
 Sometimes
␈↓ α∧␈↓parentheses must be added to insure unique decomposition.

␈↓ α∧␈↓␈↓ αTThe␈α⊂semantics␈α⊂of␈α⊂conditional␈α⊃expression␈α⊂terms␈α⊂is␈α⊂given␈α⊃by␈α⊂a␈α⊂rule␈α⊂for␈α⊃determining␈α⊂their
␈↓ α∧␈↓values.␈α
 Namely,␈αif␈α
␈↓↓p␈↓␈α
is␈αtrue,␈α
the␈α
the␈αvalue␈α
of␈α
␈↓↓IF␈αp␈α
THEN␈α
a␈αELSE␈α
b␈↓␈α
is␈αthe␈α
value␈α
of␈α␈↓↓a.␈↓␈α
Otherwise
␈↓ α∧␈↓it is the value of ␈↓↓b.␈↓

␈↓ α∧␈↓␈↓ αTIt␈α∪is␈α∪also␈α∪necessary␈α∪to␈α∪add␈α∪rules␈α∪of␈α∪inference␈α∪to␈α∪the␈α∪logic␈α∪concerned␈α∪with␈α∩conditional
␈↓ α∧␈↓expressions.␈α∞ One␈α∂could␈α∞get␈α∂by␈α∞with␈α∞rules␈α∂permitting␈α∞the␈α∂elimination␈α∞of␈α∂conditional␈α∞expressions
␈↓ α∧␈↓from␈α∂sentences␈α∞and␈α∂their␈α∞introduction.␈α∂ These␈α∞rules␈α∂are␈α∞important␈α∂anyway,␈α∞because␈α∂they␈α∞permit
␈↓ α∧␈↓proof␈α⊂of␈α⊂the␈α⊂metatheorem␈α⊃that␈α⊂the␈α⊂main␈α⊂properties␈α⊂of␈α⊃first␈α⊂order␈α⊂logic␈α⊂are␈α⊂unaffected␈α⊃by␈α⊂the
␈↓ α∧␈↓addition␈α∩of␈α⊃conditional␈α∩expressions.␈α∩ These␈α⊃include␈α∩completeness,␈α⊃the␈α∩deduction␈α∩theorem,␈α⊃and
␈↓ α∧␈↓semi-decidability.

␈↓ α∧␈↓␈↓ αTIn␈α
order␈α
to␈α
state␈α
these␈α
rules␈α
it␈α
is␈α
convenient␈α
to␈α
introduce␈α
conditional␈α
expressions␈α
also␈α∞as␈α
a
␈↓ α∧␈↓ternary␈αlogical␈αconnective.␈α A␈α
more␈αfastidious␈αexposition␈αwould␈α
use␈αa␈αdifferent␈αnotation␈αfor␈α
logical
␈↓ α∧␈↓conditional␈αexpressions,␈αbut␈αwe␈α
will␈αuse␈αthem␈αso␈α
little␈αthat␈αwe␈αmight␈α
as␈αwell␈αuse␈αthe␈αsame␈α
notation,
␈↓ α∧␈↓especially␈αsince␈α
it␈αis␈α
not␈αambiguous.␈α
 Namely,␈αif␈α
␈↓↓p,␈↓␈α␈↓↓q,␈↓␈αand␈α
␈↓↓r␈↓␈αare␈α
wffs,␈αthen␈α
so␈αis␈α
␈↓↓IF␈αp␈α
THEN␈αq
␈↓ α∧␈↓↓ELSE␈α∩r␈↓.␈α∪ Its␈α∩semantics␈α∪is␈α∩given␈α∩by␈α∪considering␈α∩it␈α∪as␈α∩a␈α∪synonym␈α∩for␈α∩␈↓↓((p␈α∪∧␈α∩q)␈α∪∨␈α∩(¬p␈α∪∧␈α∩r))␈↓.
␈↓ α∧␈↓Elimination of conditional expressions is made possible by the distributive laws

␈↓ α∧␈↓7)␈↓ αt ␈↓↓f(IF p THEN a ELSE b) = IF p THEN f(a) ELSE f(b)␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓8)␈↓ αt  ␈↓↓P(IF p THEN a ELSE b)␈↓ ε$≡ IF p THEN P(a) ELSE P(b)␈↓

␈↓ α∧␈↓␈↓ ε$≡ (p ∧ P(a)) ∨ (¬p ∧ P(b))
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ u6


␈↓ α∧␈↓where␈α∞␈↓↓f␈↓␈α∞and␈α∞␈↓↓P␈↓␈α∞stand␈α∞for␈α∞arbitrary␈α∞function␈α∞and␈α∞predicate␈α∞symbols␈α∂respectively.␈α∞ Corresponding
␈↓ α∧␈↓distributive␈α
rules␈α
are␈α
needed␈αfor␈α
functions␈α
and␈α
predicates␈α
of␈αseveral␈α
arguments␈α
when␈α
one␈α
of␈αthe
␈↓ α∧␈↓arguments␈α
is␈α
a␈α
conditional␈α
expression.␈α
 It␈α
is␈α
easy␈α
to␈α
see␈α
that␈α
application␈α
of␈α
these␈α
rules␈α
preserves␈α
the
␈↓ α∧␈↓value of a term or the truth-value of a wff.

␈↓ α∧␈↓␈↓ αTNotice␈α
that␈α
this␈αaddition␈α
to␈α
the␈αlogic␈α
has␈α
nothing␈αto␈α
do␈α
with␈αpartial␈α
functions␈α
or␈αthe␈α
element
␈↓ α∧␈↓␈↓πT␈↓.

␈↓ α∧␈↓␈↓ αTWhile␈αthe␈αabove␈αrules␈αare␈αsufficient␈αto␈αpreserve␈αthe␈αcompleteness␈αof␈αfirst␈αorder␈αlogic,␈αproofs
␈↓ α∧␈↓are␈α∂often␈α∂greatly␈α⊂shortened␈α∂by␈α∂using␈α⊂the␈α∂additional␈α∂rules␈α⊂introduced␈α∂in␈α∂(McCarthy␈α⊂1963).␈α∂ We
␈↓ α∧␈↓mention␈α
especially␈α
an␈α
extended␈α
form␈α
of␈αthe␈α
rule␈α
for␈α
replacing␈α
an␈α
expression␈α
by␈αanother␈α
expression
␈↓ α∧␈↓proved␈α
equal␈αto␈α
it.␈α Suppose␈α
we␈αwant␈α
to␈αreplace␈α
the␈αexpression␈α
␈↓↓c␈↓␈αby␈α
an␈αexpression␈α
␈↓↓c'␈↓␈α
within␈αthe
␈↓ α∧␈↓conditional␈αexpression␈α␈↓↓IF␈αp␈αTHEN␈αa␈αELSE␈αb␈↓.␈α To␈αreplace␈αan␈αoccurrence␈αof␈α␈↓↓c␈↓␈αwithin␈α␈↓↓a,␈↓␈αwe␈αneed
␈↓ α∧␈↓not␈αprove␈α
␈↓↓c = c'␈↓␈αbut␈α
merely␈α␈↓↓p ⊃ c = c'␈↓.␈α
 Likewise␈αif␈αwe␈α
want␈αto␈α
replace␈αan␈α
occurrence␈αof␈α
␈↓↓c␈↓␈αin␈α␈↓↓b,␈↓␈α
we
␈↓ α∧␈↓need only prove ␈↓↓¬p ⊃ c = c'␈↓.  This principle is further extended in the afore-mentioned paper.

␈↓ α∧␈↓␈↓ αTA␈α⊃further␈α⊂useful␈α⊃and␈α⊂eliminable␈α⊃extension␈α⊂to␈α⊃the␈α⊂logic␈α⊃is␈α⊂to␈α⊃allow␈α⊂"first␈α⊃order"␈α⊂lambda
␈↓ α∧␈↓expressions␈α∂as␈α∂function␈α∂and␈α∂predicate␈α∂expressions.␈α∂ Thus␈α∞if␈α∂␈↓↓x␈↓␈α∂is␈α∂an␈α∂individula␈α∂variable,␈α∂␈↓↓e␈↓␈α∂is␈α∞a
␈↓ α∧␈↓term,␈α
and␈α␈↓↓p␈↓␈α
is␈αa␈α
wff,␈αthen␈α
␈↓↓λx.e␈↓␈α
and␈α␈↓↓λx.p␈↓␈α
may␈αbe␈α
used␈αwherever␈α
a␈αfunction␈α
symbol␈α
or␈αpredicate
␈↓ α∧␈↓symbol␈α∂respectively␈α∞are␈α∂allowed.␈α∞ The␈α∂only␈α∞rule␈α∂required␈α∞is␈α∂lambda␈α∞conversion␈α∂which␈α∂serves␈α∞to
␈↓ α∧␈↓eliminate␈α⊂or␈α⊂introduce␈α⊂lambda␈α∂expressions.␈α⊂ (We␈α⊂assume␈α⊂that␈α∂the␈α⊂rules␈α⊂for␈α⊂lambda␈α∂conversion
␈↓ α∧␈↓include␈α
alphabetic␈α
changes␈αof␈α
bound␈α
variables␈αwhen␈α
needed␈α
to␈α
avoid␈αcapture␈α
of␈α
the␈αfree␈α
variables
␈↓ α∧␈↓in arguments of lambda expressions).

␈↓ α∧␈↓␈↓ αTThe␈α∞use␈α∞of␈α∞minimization␈α
schemata␈α∞and␈α∞schemata␈α∞of␈α
induction␈α∞is␈α∞facilitated␈α∞by␈α∞first␈α
order
␈↓ α∧␈↓lambda␈αexressions,␈αsince␈αthe␈αsubstitution␈αjust␈αreplaces␈αoccurrences␈αof␈αthe␈αfunction␈αvariable␈α
in␈αthe
␈↓ α∧␈↓schema␈α⊂by␈α⊃a␈α⊂lambda␈α⊃expression␈α⊂which␈α⊂can␈α⊃subsequently␈α⊂be␈α⊃expanded␈α⊂by␈α⊃lambda␈α⊂conversion.
␈↓ α∧␈↓Without␈α∞lambda␈α∞expressions␈α∞the␈α∞rule␈α∞for␈α∞substitution␈α∞in␈α∞schemata␈α∞is␈α∞complicated␈α∞to␈α∞state.␈α∞ First
␈↓ α∧␈↓order␈α
lambda␈α
expressions␈α
also␈α
permit␈α
many␈α
sentences␈αto␈α
be␈α
expressed␈α
more␈α
compactly␈α
as␈α
well␈αas
␈↓ α∧␈↓being␈α∪required␈α∪to␈α∪avoid␈α∩duplicate␈α∪computations␈α∪in␈α∪recursive␈α∩programs.␈α∪ Thus␈α∪we␈α∪can␈α∩write
␈↓ α∧␈↓␈↓↓[λx.x␈↓#
2␈↓# + x](a + b)␈↓␈α⊗instead␈α∃of␈α⊗␈↓↓(a + b)␈↓#
2␈↓# + (a + b)␈↓.␈α∃ Since␈α⊗all␈α∃occurrences␈α⊗of␈α∃first␈α⊗order␈α∃lambda
␈↓ α∧␈↓expressions␈α∞can␈α
be␈α∞eliminated␈α
from␈α∞wffs␈α
by␈α∞lambda␈α
conversion,␈α∞the␈α
metatheorems␈α∞of␈α∞first␈α
order
␈↓ α∧␈↓logic␈αare␈α
again␈αpreserved.␈α The␈α
reason␈αwe␈α
don't␈αget␈αthe␈α
full␈αlambda␈αcalculus␈α
is␈αthat␈α
the␈αsyntactic
␈↓ α∧␈↓rules␈αof␈αfirst␈αorder␈αlogic␈αprevent␈αa␈αvariable␈αfrom␈αbeing␈αused␈αin␈αboth␈αterm␈αand␈αfunction␈αpositions.
␈↓ α∧␈↓While␈αwe␈αhave␈αillustrated␈αthe␈αuse␈αof␈αlambda␈αexpressions␈αwith␈αsingle␈αvariable␈αλ's,␈αexpressions␈αlike
␈↓ α∧␈↓␈↓↓λx y z.e␈↓␈α
are␈α
also␈α
useful␈αand␈α
give␈α
no␈α
trouble.␈α It␈α
is␈α
also␈α
easily␈αseen␈α
that␈α
lambda␈α
conversion␈αwithin␈α
a
␈↓ α∧␈↓term preserves its value, and lambda conversion within a wff preserves its truth value.

␈↓ α∧␈↓␈↓ αTActually␈α
it␈α
seems␈α
that␈α
even␈α
higher␈α
order␈α
λ's␈α
won't␈α
get␈α
us␈α
out␈α
of␈α
first␈α
order␈α
logic␈α
provided
␈↓ α∧␈↓rules␈α
of␈α
typing␈αare␈α
obeyed␈α
and␈αwe␈α
provide␈α
no␈αway␈α
of␈α
quantifying␈αover␈α
function␈α
variables.␈α Any
␈↓ α∧␈↓occurrences␈α∞of␈α∞higher␈α∞order␈α
lambda␈α∞expressions␈α∞in␈α∞wffs␈α∞are␈α
eliminable␈α∞just␈α∞by␈α∞carrying␈α∞out␈α
the
␈↓ α∧␈↓indicated lambda conversions.  For example, we could define

␈↓ α∧␈↓␈↓ αT␈↓↓transitive = λπ.(∀X Y Z.(π(X,Y) ∧ π(Y,Z) ⊃ π(X,Z)))␈↓,

␈↓ α∧␈↓and any use of ␈↓↓transitive␈↓ in a wff would be eliminable using its definition and lambda conversion.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ u7


␈↓ α∧␈↓α4. Partial Functions and Partial Predicates.

␈↓ α∧␈↓␈↓ αTThe␈αmain␈αdifficulty␈αto␈αbe␈αovercome␈αin␈αrepresenting␈αrecursive␈αprograms␈αby␈αlogical␈αsentences
␈↓ α∧␈↓is␈α⊂that␈α∂the␈α⊂computation␈α∂of␈α⊂an␈α∂arbitrary␈α⊂recursive␈α∂program␈α⊂cannot␈α∂be␈α⊂guaranteed␈α⊂to␈α∂terminate.
␈↓ α∧␈↓Consider the recursive definition

␈↓ α∧␈↓9)␈↓ αt ␈↓↓f n ← f n +1␈↓

␈↓ α∧␈↓over the integers.  If we translate it into the sentence

␈↓ α∧␈↓10)␈↓ αt ␈↓↓∀n.(f(n) = f(n) +1)␈↓

␈↓ α∧␈↓and use the axioms of arithmetic, we get a contradiction.

␈↓ α∧␈↓␈↓ αTThe␈α∂way␈α∂out␈α∂is␈α∂to␈α∂adjoin␈α∂to␈α∞our␈α∂data␈α∂domains␈α∂an␈α∂additional␈α∂element␈α∂␈↓πT␈↓␈α∂(read␈α∞"bottom"),
␈↓ α∧␈↓which␈α∞is␈α∞taken␈α∞to␈α∞be␈α∞the␈α∞value␈α∞of␈α∞the␈α∞function␈α∞when␈α∞the␈α∞computation␈α∞doesn't␈α∂terminate.␈α∞ Then
␈↓ α∧␈↓going from (9) to (10) doesn't lead to a contradiction but to the desired result that

␈↓ α∧␈↓11)␈↓ αt ␈↓↓∀n.(f(n) = ␈↓πT␈↓↓)␈↓,

␈↓ α∧␈↓provided we also postulate that

␈↓ α∧␈↓12)␈↓ αt ␈↓↓∀n.(n + ␈↓πT␈↓↓ = ␈↓πT␈↓↓ + n = ␈↓πT␈↓↓)␈↓,

␈↓ α∧␈↓which␈α⊂is␈α⊂reasonable␈α⊂given␈α⊂the␈α⊂interpretation␈α⊂of␈α∂␈↓πT␈↓␈α⊂as␈α⊂the␈α⊂value␈α⊂of␈α⊂a␈α⊂computation␈α⊂that␈α∂doesn't
␈↓ α∧␈↓terminate.␈α
 We␈α
will␈α
postulate␈αthat␈α
all␈α
of␈α
the␈α
base␈αfunctions,␈α
except␈α
the␈α
conditional␈αexpression,␈α
have
␈↓ α∧␈↓␈↓πT␈↓ as value if any argument is ␈↓πT␈↓.  Such functions are called ␈↓↓strict␈↓.

␈↓ α∧␈↓␈↓ αTWe␈α
have␈α
discussed␈α
treating␈αpartial␈α
functions␈α
by␈α
introducing␈α
␈↓πT␈↓.␈α A␈α
function␈α
take␈α
the␈αvalue␈α
␈↓πT␈↓
␈↓ α∧␈↓when␈α∞the␈α∞program␈α∞that␈α∞computes␈α∞it␈α∞doesn't␈α∞terminate,␈α∞and␈α∞it␈α∞is␈α∞sometimes␈α∞convenient␈α∞to␈α∂give␈α∞a
␈↓ α∧␈↓function the value ␈↓πT␈↓ in some other cases when we want it to be undefined.

␈↓ α∧␈↓␈↓ αTIt␈α
is␈α
convenient␈α
to␈α
introduce␈α
a␈α
rather␈α
trivial␈α
partial␈α
ordering␈α
relation␈α
on␈α
our␈α
data␈αdomain
␈↓ α∧␈↓once it has been extended by adjoining ␈↓πT␈↓.  Namely, we define the relation ␈↓↓X ␈↓πa␈↓↓ Y␈↓ by

␈↓ α∧␈↓13)␈↓ αt ␈↓↓∀X Y.(X ␈↓πa␈↓↓ Y ≡ X = ␈↓πT␈↓↓ ∧ y ≠ ␈↓πT␈↓↓)␈↓

␈↓ α∧␈↓and␈α
make␈α
corresponding␈α
definitions␈α
of␈α
␈↓πc␈↓,␈α
␈↓πb␈↓,␈α
and␈α
␈↓πd␈↓.␈α
 The␈α
ordering␈α
can␈α
be␈α
extended␈α
to␈α
functions␈α
by
␈↓ α∧␈↓postulating that

␈↓ α∧␈↓14)␈↓ αt ␈↓↓f ␈↓πb␈↓↓ g ≡ ∀X.(f(X) ␈↓πb␈↓↓ g(X))␈↓.

␈↓ α∧␈↓This␈αinduced␈αordering␈α
is␈αnot␈αso␈αtrivial,␈α
but␈αwe␈αwon't␈α
use␈αit␈αin␈αour␈α
formal␈αtheory,␈αbecause␈α
it␈αisn't
␈↓ α∧␈↓first␈α⊂order.␈α⊂ Even␈α⊃though␈α⊂(13)␈α⊂defines␈α⊂a␈α⊃rather␈α⊂trivial␈α⊂ordering,␈α⊂we␈α⊃find␈α⊂that␈α⊂it␈α⊃shortens␈α⊂and
␈↓ α∧␈↓clarifies many formulas.

␈↓ α∧␈↓␈↓ αTPartial␈α⊂predicates␈α⊂give␈α∂rise␈α⊂to␈α⊂new␈α∂problems.␈α⊂ The␈α⊂computation␈α∂of␈α⊂a␈α⊂recursively␈α∂defined
␈↓ α∧␈↓predicate␈αmay␈αnot␈αterminate,␈αso␈αthe␈αsame␈α
problem␈αarises.␈α However,␈αwe␈αcan't␈αsolve␈αit␈αin␈α
the␈αsame
␈↓ α∧␈↓way␈αwithout␈αadding␈α
an␈αadditional␈αundefined␈α
truth␈αvalue␈αto␈α
the␈αlogic.␈α This␈α
would␈αgive␈αrise␈α
to␈αa
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ u8


␈↓ α∧␈↓partial␈α⊂first␈α∂order␈α⊂logic␈α∂in␈α⊂which␈α⊂sentences␈α∂could␈α⊂be␈α∂true,␈α⊂false␈α∂or␈α⊂undefined.␈α⊂ Various␈α∂partial
␈↓ α∧␈↓predicate␈αcalculi␈αhave␈αbeen␈αstudied␈αin␈α(McCarthy␈α1964)␈αand␈αelsewhere,␈αbut␈αthey␈αhave␈αthe␈αserious
␈↓ α∧␈↓disadvantage␈α⊂that␈α⊂arguments␈α⊂by␈α⊂cases␈α⊂become␈α⊂quite␈α⊂long,␈α⊂since␈α⊂three␈α⊂cases␈α⊂always␈α⊂have␈α⊂to␈α∂be
␈↓ α∧␈↓provided␈α
for,␈α
even␈α
when␈α
most␈α
of␈α
the␈α
predicates␈α
are␈α
known␈α
to␈α
be␈α
total.␈α
 Moreover,␈α
existing␈αlogic
␈↓ α∧␈↓texts,␈α∞proof-checkers␈α
and␈α∞theorem␈α
provers␈α∞all␈α
use␈α∞total␈α
logic.␈α∞ Therefore,␈α
it␈α∞seems␈α
better␈α∞to␈α
keep
␈↓ α∧␈↓the logic conventional and handle partial predicates as functions.

␈↓ α∧␈↓␈↓ αTWe␈αintroduce␈αa␈αdomain␈α␈↓	P␈↓␈αwith␈αthree␈αelements␈α␈↓↓T,␈↓␈α␈↓↓F␈↓␈αand␈α␈↓πT␈↓␈αcalled␈αthe␈αdomain␈αof␈αextended
␈↓ α∧␈↓truth␈α
values.␈α
 In␈α
a␈α
sorted␈α
logic,␈α
this␈α
may␈α
be␈α
a␈α
separate␈α
sort.␈α
 Otherwise,␈α
it␈α
may␈α
be␈αconsidered␈α
either
␈↓ α∧␈↓separately␈α∞or␈α
as␈α∞part␈α∞of␈α
the␈α∞main␈α∞data␈α
domain.␈α∞ In␈α
Lisp␈α∞it␈α∞is␈α
convenient␈α∞to␈α∞regard␈α
␈↓↓T␈↓␈α∞and␈α∞␈↓↓F␈↓␈α
as
␈↓ α∧␈↓special␈α
atoms␈α
and␈α
to␈α
use␈α
the␈α
same␈α
␈↓πT␈↓␈α
for␈α
extended␈α
truth␈α
values␈α
as␈α
for␈α
extended␈α
S-expressions.␈α It␈α
is
␈↓ α∧␈↓even␈α
possible␈α∞to␈α
follow␈α
the␈α∞Lisp␈α
implementations␈α∞that␈α
use␈α
NIL␈α∞for␈α
␈↓↓F␈↓␈α
and␈α∞interpret␈α
all␈α∞other␈α
S-
␈↓ α∧␈↓expressions as ␈↓↓T,␈↓ although we don't do that in this paper.

␈↓ α∧␈↓␈↓ αTIt␈α
is␈αconvenient␈α
to␈αdefine␈α
first␈α
a␈αform␈α
of␈αconditional␈α
expression␈α
that␈αtakes␈α
an␈αextended␈α
truth
␈↓ α∧␈↓value as its first argument, namely

␈↓ α∧␈↓␈↓ αT␈↓↓␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = IF p = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF p = T THEN a ELSE b␈↓.

␈↓ α∧␈↓The␈α⊂only␈α⊂difference␈α⊂between␈α⊂then␈α⊂extended␈α⊂conditional␈α⊂expression␈α⊂and␈α⊂the␈α⊂logical␈α⊂conditional
␈↓ α∧␈↓expression␈α⊂is␈α⊂that␈α⊂since␈α∂the␈α⊂extended␈α⊂conditional␈α⊂expression␈α∂takes␈α⊂an␈α⊂extended␈α⊂truth␈α⊂value␈α∂as
␈↓ α∧␈↓propositional␈αargument,␈αwe␈αcan␈αprovide␈αfor␈αthe␈αpossibility␈αthat␈αthe␈αcomputation␈αof␈αthat␈αargument
␈↓ α∧␈↓fails␈αto␈αterminate.␈α Since␈αthe␈αextended␈αconditional␈αexpression␈αtreats␈αthe␈αundefined␈αcases␈αaccording
␈↓ α∧␈↓to their behavior in programs, we use the same notation.

␈↓ α∧␈↓␈↓ αTExtended␈α∃boolean␈α⊗operators␈α∃are␈α∃conveniently␈α⊗defined␈α∃using␈α∃the␈α⊗extended␈α∃conditional
␈↓ α∧␈↓expressions.␈α⊃ For␈α⊃every␈α⊃predicate␈α⊃or␈α⊃boolean␈α⊃operator,␈α⊃we␈α⊃introduce␈α⊃a␈α⊃corresponding␈α⊃function
␈↓ α∧␈↓taking␈αextended␈αtruth␈αvalues␈αas␈αoperands␈αand␈αtaking␈αan␈αextended␈αtruth␈αvalue␈αas␈αits␈αvalue.␈α Thus
␈↓ α∧␈↓the function ␈↓↓and,␈↓ is written with an infix and defined by

␈↓ α∧␈↓␈↓ αT␈↓↓p and q = ␈↓	f␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ F

␈↓ α∧␈↓The␈αfunction␈α␈↓↓and␈↓␈αis␈αdistinct␈αfrom␈αthe␈αlogical␈αoperator␈α∧␈αwhich␈αremains␈αin␈αthe␈αlogic.␈α To␈αillustrate
␈↓ α∧␈↓this, we have the true sentence

␈↓ α∧␈↓␈↓ αT␈↓↓((p and q) = T) ≡ (p = T) ∧ (q = T).

␈↓ α∧␈↓The␈αparentheses␈α
in␈αthe␈αabove␈α
can␈αbe␈α
omitted␈αwithout␈αambiguity␈α
given␈αsuitable␈α
precedence␈αrules.
␈↓ α∧␈↓Note␈αthat␈α␈↓↓and␈↓␈αhas␈αthe␈αnon-commutative␈αproperty␈αof␈α(McCarthy␈α1963),␈αnamely␈α␈↓↓F and ␈↓πT␈↓↓ = F␈↓␈α
while
␈↓ α∧␈↓␈↓↓␈↓πT␈↓↓ and F = ␈↓πT␈↓↓␈↓.␈α This␈αcorresponds␈α
to␈αthe␈αfact␈α
that␈αit␈αis␈α
convenient␈αto␈αcompute␈α
␈↓↓p and q␈↓␈αby␈αa␈α
program
␈↓ α∧␈↓that␈α∞doesn't␈α∞look␈α∞at␈α∞␈↓↓q␈↓␈α∞if␈α∞␈↓↓p␈↓␈α∞is␈α∞false␈α∞but␈α∞which␈α∞doesn't␈α∞terminate␈α∞if␈α∞the␈α∞computation␈α∞of␈α∂␈↓↓p␈↓␈α∞doesn't
␈↓ α∧␈↓terminate.␈α Symmetry␈αcould␈αbe␈αrestored␈αif␈αthe␈αcomputer␈αtime-shared␈αits␈αcomputations␈αof␈α␈↓↓p␈↓␈αand␈α␈↓↓q,␈↓
␈↓ α∧␈↓but␈αthere␈αare␈αtoo␈αmany␈αpractical␈αdisadvantages␈αto␈αsuch␈αa␈αsystem␈αto␈αjustify␈αdoing␈αit␈αfor␈αthe␈αsake␈αof
␈↓ α∧␈↓mathematical␈αsymmetry.␈α Algol␈α60␈αrequires␈αthat␈αboth␈α␈↓↓p␈↓␈αand␈α␈↓↓q␈↓␈αbe␈αcomputed␈αwhich␈αprecludes␈αusing
␈↓ α∧␈↓boolean opeators as the main connectives of Lisp type recursive definitions of predicates.

␈↓ α∧␈↓␈↓ αTOther imitation boolean operators are defined by

␈↓ α∧␈↓␈↓ αT␈↓↓p or q = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ q␈↓
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ u9


␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓not p = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ F ␈↓αelse␈↓↓ T␈↓.

␈↓ α∧␈↓␈↓ αTWe also require an equality function that extends the equality operator, namely

␈↓ α∧␈↓␈↓ αT␈↓↓x equal y = IF x = ␈↓πT␈↓↓ ∨ y = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF x = y THEN T ELSE F␈↓.

␈↓ α∧␈↓␈↓ αTIn␈αfact,␈αthe␈αkey␈αto␈αsuccessful␈αrepresentation␈αof␈αrecursive␈αprograms␈αin␈αfirst␈αorder␈αlogic␈αis␈αthe
␈↓ α∧␈↓simultaneous␈α∂use␈α∞of␈α∂true␈α∞equality␈α∂in␈α∞the␈α∂logic␈α∂in␈α∞order␈α∂to␈α∞make␈α∂assertions␈α∞freely␈α∂and␈α∂the␈α∞␈↓↓equal␈↓
␈↓ α∧␈↓function␈α∪that␈α∪gives␈α∀an␈α∪undefined␈α∪result␈α∪for␈α∀undefined␈α∪arguments.␈α∪ The␈α∪latter␈α∀describes␈α∪the
␈↓ α∧␈↓behavior␈α∞of␈α∞an␈α∞equality␈α∞test␈α∞within␈α∞the␈α∞program.␈α∞ The␈α∞two␈α∞forms␈α∞of␈α∞conditional␈α∂expression␈α∞are
␈↓ α∧␈↓also essential.

␈↓ α∧␈↓␈↓ αTThe partial ordering ␈↓πa␈↓ is also useful applied to extended truth values.

␈↓ α∧␈↓␈↓ αTWe summarize this in the following set of axioms:

␈↓ α∧␈↓T1: ␈↓↓∀p.(istv p ≡ p = T ∨ p = F)␈↓

␈↓ α∧␈↓T2: ␈↓↓∀p.(isetv p ≡ istv p ∨ p = ␈↓πT␈↓↓)␈↓

␈↓ α∧␈↓T3: ␈↓↓T ≠ F ∧ ¬istv ␈↓πT␈↓↓␈↓

␈↓ α∧␈↓T4:␈α
␈↓↓∀p␈α
X␈αY.(isetv␈α
p␈α
⊃␈α␈↓αif␈↓↓␈α
p␈α
␈↓αthen␈↓↓␈αX␈α
␈↓αelse␈↓↓␈α
Y␈α=␈α
IF␈α
p␈α
=␈α␈↓πT␈↓↓␈α
THEN␈α
␈↓πT␈↓↓␈αELSE␈α
IF␈α
p␈α=␈α
T␈α
THEN␈αX␈α
ELSE
␈↓ α∧␈↓↓Y␈↓

␈↓ α∧␈↓T5: ␈↓↓∀p.(isetv p ⊃ not p = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ F ␈↓αelse␈↓↓ T)␈↓

␈↓ α∧␈↓T6: ␈↓↓∀p q.(isetv p ∧ isetv q ⊃ p and q = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ F)␈↓

␈↓ α∧␈↓T7: ␈↓↓∀p q.(isetv p ∧ isetv q ⊃ p or q = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ q)␈↓

␈↓ α∧␈↓T8: ␈↓↓∀X Y.(X equal Y = IF X = ␈↓πT␈↓↓ ∨ Y = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF X = Y THEN T ELSE F␈↓

␈↓ α∧␈↓T9: ␈↓↓∀p.(isetv p ∧ isetv q ⊃ (p ␈↓πa␈↓↓ q ≡ p = ␈↓πT␈↓↓ ∧ (q = T ∨ q = F)))␈↓.




␈↓ α∧␈↓α5. The Functional Equation of a Recursive Program - Theory.

␈↓ α∧␈↓␈↓ αTThe familiar recursive program

␈↓ α∧␈↓15)␈↓ αt ␈↓↓u * v ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓

␈↓ α∧␈↓is a special case of a system of mutually recursive programs which can be written

␈↓ α∧␈↓16)␈↓ αt␈↓ αt␈↓↓f␈↓#v1␈↓#(x␈↓#v1␈↓#,...,x␈↓#vm␈↓#l1␈↓#v␈↓#) ← ␈↓	t␈↓↓␈↓#v1␈↓#(f␈↓#v1␈↓#, ... ,f␈↓#vn␈↓#,x␈↓#v1␈↓#, ... ,x␈↓#vm␈↓#l1␈↓#v␈↓#)␈↓
␈↓ α∧␈↓␈↓ αT␈↓ αt.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f10


␈↓ α∧␈↓␈↓ αT␈↓ αt.
␈↓ α∧␈↓␈↓ αT␈↓ αt.
␈↓ α∧␈↓␈↓ αT␈↓ αt␈↓↓f␈↓#vn␈↓#(x␈↓#v1␈↓#,...,x␈↓#vm␈↓#ln␈↓#v␈↓#) ← ␈↓	t␈↓↓␈↓#v1␈↓#(f␈↓#v1␈↓#, ... ,f␈↓#vn␈↓#,x␈↓#v1␈↓#, ... ,x␈↓#vm␈↓#ln␈↓#v␈↓#)␈↓.

␈↓ α∧␈↓Here␈α
the␈α∞␈↓	t␈↓'s␈α
are␈α∞terms␈α
in␈α∞the␈α
individual␈α∞variables␈α
␈↓↓x␈↓#v1␈↓#␈↓,␈α∞etc.␈α
and␈α∞the␈α
function␈α∞symbols␈α
␈↓↓f␈↓#v1␈↓#, ... f␈↓#vn␈↓#␈↓.
␈↓ α∧␈↓All␈α∩the␈α∩essential␈α∩features␈α∩of␈α∩such␈α∩mutual␈α∩recursive␈α∩definitions␈α∩arise␈α∩when␈α∩there␈α∩is␈α∪only␈α∩one
␈↓ α∧␈↓equation,␈α
but␈α
phenomena␈α
arise␈α
when␈α
there␈α
are␈α
two␈α
or␈α
more␈α
arguments␈α
to␈α
the␈α
functions␈α
that␈αdo␈α
not
␈↓ α∧␈↓arise in the one argument case - two arguments being sufficiently general.  Therefore, we write

␈↓ α∧␈↓17)␈↓ αt ␈↓↓f(x,y) ← ␈↓	t␈↓↓(f,x,y)␈↓,

␈↓ α∧␈↓which may also be written

␈↓ α∧␈↓18)␈↓ αt ␈↓↓ f(x,y) ← ␈↓	t␈↓↓[f](x,y)␈↓

␈↓ α∧␈↓when we wish to emphasize that ␈↓	t␈↓ maps a partial function ␈↓↓f␈↓ into another partial function ␈↓↓␈↓	t␈↓↓[f]␈↓.

␈↓ α∧␈↓␈↓ αTSuch␈α∞a␈α
program␈α∞or␈α
system␈α∞of␈α∞mutually␈α
recursive␈α∞programs␈α
can␈α∞be␈α
regarded␈α∞as␈α∞defining␈α
a
␈↓ α∧␈↓partial function in several ways.

␈↓ α∧␈↓1.␈α
It␈α
can␈α
be␈α∞compiled␈α
into␈α
a␈α
machine␈α
language␈α∞program␈α
for␈α
some␈α
computer␈α∞using␈α
call-by-value.
␈↓ α∧␈↓The␈α
resulting␈α
program␈α
is␈α
a␈αsubroutine␈α
that␈α
calls␈α
itself␈α
recursively.␈α Before␈α
it␈α
is␈α
called,␈α
the␈αvalues␈α
of
␈↓ α∧␈↓the␈αarguments␈α
must␈αbe␈α
computed␈αand␈α
stored␈αin␈α
suitable␈αconventional␈α
registers.␈α This␈α
includes␈αits
␈↓ α∧␈↓calls␈αto␈αitself.␈α Most␈αLisp␈αimplementations␈αas␈αwell␈αas␈αmost␈αimplementations␈αin␈αother␈αprogramming
␈↓ α∧␈↓languages use call-by-value.

␈↓ α∧␈↓2.␈α
It␈α
can␈α∞be␈α
compiled␈α
into␈α∞a␈α
machine␈α
language␈α
program␈α∞for␈α
some␈α
computer␈α∞using␈α
call-by-name.
␈↓ α∧␈↓The␈α
resulting␈α
program␈α
again␈αcalls␈α
itself␈α
recursively.␈α
 It␈α
is␈αcalled␈α
by␈α
storing␈α
into␈α
suitable␈αregisters
␈↓ α∧␈↓the␈α
location␈αof␈α
programs␈αfor␈α
computing␈α
the␈αexpressions␈α
that␈αhave␈α
been␈αwritten␈α
as␈α
its␈αarguments.
␈↓ α∧␈↓Thus␈α␈↓↓((w.z)*f(u))␈↓␈αwould␈αbe␈αcompiled␈αinto␈αprogram␈αthat␈αwould␈αgive␈αthe␈αprogram␈αfor␈α␈↓↓u*v␈↓␈αpointers
␈↓ α∧␈↓to␈α⊂program␈α⊂for␈α∂computing␈α⊂␈↓↓w.z␈↓␈α⊂and␈α∂␈↓↓f(u).␈↓␈α⊂The␈α⊂program␈α∂for␈α⊂*␈α⊂could␈α∂call␈α⊂these␈α⊂other␈α∂programs
␈↓ α∧␈↓whenever␈α∪it␈α∩wanted␈α∪its␈α∪arguments.␈α∩ In␈α∪the␈α∩case␈α∪of␈α∪␈↓↓u*v,␈↓␈α∩there␈α∪is␈α∩nothing␈α∪the␈α∪program␈α∩can
␈↓ α∧␈↓profitably␈α⊂do␈α∂except␈α⊂call␈α⊂for␈α∂both␈α⊂of␈α⊂its␈α∂arguments.␈α⊂ However,␈α⊂a␈α∂program␈α⊂for␈α⊂multiplying␈α∂two
␈↓ α∧␈↓matrices␈αmight␈αcall␈αits␈αfirst␈αargument,␈αand,␈αif␈αthe␈αfirst␈αargument␈αturned␈αout␈αto␈αbe␈αthe␈αzero␈αmatrix,
␈↓ α∧␈↓not bother to call the second argument.

␈↓ α∧␈↓We␈αcan␈αalso␈α
consider␈αevaluating␈αthe␈α
function␈αby␈αsymbolic␈α
computation.␈α Namely,␈αwe␈αsubstitute␈α
the
␈↓ α∧␈↓arguments␈αof␈α
the␈αfunction␈α*␈α
for␈α␈↓↓u␈↓␈α
and␈α␈↓↓v,␈↓␈αand␈α
then␈αevaluate␈α
the␈αright␈αhand␈α
side␈αof␈αthe␈α
definition.
␈↓ α∧␈↓There␈αare␈αmany␈αways␈αto␈αdo␈αthis␈αevalution,␈αbecause␈αthere␈αmay␈αbe␈αmore␈αthan␈αone␈αoccurrence␈αof␈α
the
␈↓ α∧␈↓function␈α
being␈α
defined␈α∞on␈α
the␈α
right␈α
hand␈α∞side␈α
of␈α
the␈α
definition,␈α∞but␈α
two␈α
of␈α
them␈α∞correspond␈α
to
␈↓ α∧␈↓call-by-name and call-by-value respectively.

␈↓ α∧␈↓3.␈α
When␈α
evaluating␈α
a␈αconditional␈α
expression,␈α
always␈α
evalute␈α
the␈αpropositional␈α
term␈α
first␈α
and␈αuse␈α
it
␈↓ α∧␈↓to␈α∪decide␈α∪which␈α∪of␈α∪the␈α∪other␈α∪terms␈α∪to␈α∪evaluate␈α∪first.␈α∪ When␈α∪evaluating␈α∪a␈α∪term␈α∀formed␈α∪by
␈↓ α∧␈↓composition␈α
of␈α
functions,␈α
if␈α
there␈α
is␈α
only␈αone␈α
occurrence␈α
of␈α
the␈α
function␈α
being␈α
defined␈α
on␈αthe␈α
right
␈↓ α∧␈↓hand␈α∂side,␈α∂there␈α∂is␈α⊂no␈α∂choice␈α∂to␈α∂be␈α⊂made,␈α∂but␈α∂if␈α∂there␈α∂is␈α⊂more␈α∂than␈α∂one,␈α∂expand␈α⊂the␈α∂leftmost
␈↓ α∧␈↓innermost␈α∞first.␈α∞ If␈α∞it␈α∞gives␈α∞an␈α∞answer␈α∂subsitute␈α∞it␈α∞and␈α∞continue␈α∞the␈α∞process.␈α∞ If␈α∞it␈α∂gives␈α∞further
␈↓ α∧␈↓recursion, then proceed with its leftmost innermost, etc.  This corresponds to call-by value.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f11


␈↓ α∧␈↓4.␈αIf␈αinstead␈αof␈αexpanding␈αthe␈αleftmost␈αinnermost␈αoccurrence␈αof␈αthe␈αfunction␈αfirst,␈αwe␈αexpand␈αthe
␈↓ α∧␈↓outermost occurrences, we get an evaluation method corresponding to call-by-name.

␈↓ α∧␈↓␈↓ αTIt␈α∂is␈α∂proved␈α∂in␈α∂(xxx)␈α∂that␈α∂evaluation␈α∂by␈α∂substitution␈α∂and␈α∂evaluation␈α∂by␈α⊂subroutine␈α∂both
␈↓ α∧␈↓using␈α∂call-by-value␈α∂give␈α∂the␈α∂same␈α∂results.␈α⊂ The␈α∂two␈α∂ways␈α∂of␈α∂doing␈α∂call-by-name␈α∂also␈α⊂give␈α∂the
␈↓ α∧␈↓same results.

␈↓ α∧␈↓␈↓ αTComputing␈α∀␈↓↓u*v␈↓␈α∀doesn't␈α∪show␈α∀the␈α∀difference␈α∀between␈α∪these␈α∀methods,␈α∀but␈α∀consider␈α∪the
␈↓ α∧␈↓function

␈↓ α∧␈↓19)␈↓ αt ␈↓↓cadiou(x,y) ← ␈↓αif␈↓↓ x = 0 ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ cadiou(x - 1, cadiou(x + 1, y))␈↓.

␈↓ α∧␈↓Evaluating␈α
␈↓↓cadiou(2,1)␈↓␈α
by␈α
either␈α
call-by-value␈α
method␈α
leads␈α
to␈α
an␈α
infinite␈α
computation,␈α
because
␈↓ α∧␈↓the␈αterm␈α␈↓↓cadiou(x + 1, y)␈↓␈αhas␈αto␈αbe␈αevaluated␈αand␈αleads␈αus␈αfurther␈αand␈αfurther␈αfrom␈αtermination.
␈↓ α∧␈↓Call-by-name␈αevaluation,␈αon␈αthe␈αother␈αhand,␈αgives␈αthe␈αanswer␈α0,␈αbecause␈αthe␈αsecond␈αargument␈αof
␈↓ α∧␈↓␈↓↓cadiou␈↓␈αis␈αnever␈α
called.␈α Vuillemin␈α(1973)␈α
shows␈αthat␈αwhenever␈α
call-by-value␈αgives␈αan␈αanswer,␈α
call-
␈↓ α∧␈↓by-name␈αgives␈αthe␈αsame␈αanswer,␈αbut␈αsometimes␈αcall-by-name␈αgives␈αan␈αanswer␈αwhen␈αcall-by-value
␈↓ α∧␈↓doesn't.␈α If␈αwe␈αforce␈αa␈αprogram␈αto␈αbe␈α␈↓↓strict,␈↓␈αi.e.␈α to␈αdemand␈αthat␈αall␈αof␈αits␈αarguments␈αare␈αdefined,
␈↓ α∧␈↓then call-by-name and call-by-value are equi-terminating - to coin a word.

␈↓ α∧␈↓␈↓ αT(Manna 1974) also contains proofs of these assertions.

␈↓ α∧␈↓␈↓ αTExecution␈α⊗of␈α⊗recursive␈α⊗programs␈α⊗by␈α∃substitution␈α⊗is␈α⊗inefficient,␈α⊗but␈α⊗provides␈α⊗a␈α∃good
␈↓ α∧␈↓theoretical tool for classifying the more efficient subroutine methods of evaluation.

␈↓ α∧␈↓5.␈α
Finally,␈αwe␈α
can␈α
regard␈α(15)␈α
and␈α
(16)␈αas␈α
functional␈αequations␈α
for␈α
*␈αand␈α
␈↓↓cadiou␈↓␈α
respectively.␈α In
␈↓ α∧␈↓general,␈α∞a␈α∞functional␈α∞equation␈α∞may␈α∞have␈α∞many␈α∞solutions␈α∞or␈α∞none.␈α∞ However,␈α∞it␈α∞has␈α∞been␈α
shown
␈↓ α∧␈↓(see␈α∞Manna␈α∞1974)␈α∞that␈α∞if␈α∞the␈α∞right␈α∞side␈α∞is␈α∞␈↓↓continuous␈↓␈α∞in␈α∞the␈α∞function␈α∞being␈α∞defined␈α∞and␈α∞in␈α∞the
␈↓ α∧␈↓individual␈α∞variables,␈α∞there␈α∞will␈α∂be␈α∞a␈α∞unique␈α∞␈↓↓minimal␈↓␈α∞solution.␈α∂ This␈α∞condition␈α∞is␈α∞assured␈α∂if␈α∞the
␈↓ α∧␈↓right␈α⊃hand␈α⊃side␈α⊃is␈α⊃a␈α⊃term␈α⊃built␈α⊃from␈α⊃strict␈α⊃functions␈α⊃and␈α⊃predicates␈α⊃by␈α⊃composition␈α⊃and␈α⊃the
␈↓ α∧␈↓formation␈α∀of␈α∀extended␈α∪conditional␈α∀expresions.␈α∀ We␈α∪won't␈α∀discuss␈α∀continuity␈α∪here.␈α∀ It␈α∀is␈α∪not
␈↓ α∧␈↓permitted␈α
to␈α
use␈α
logical␈α
conditional␈α
expression,␈αand␈α
this␈α
restriction␈α
prevents␈α
true␈α
equality␈α
or␈αany
␈↓ α∧␈↓predicate␈α
from␈α
direct␈α
use.␈α If␈α
true␈α
conditional␈α
expressions␈αwere␈α
allowed,␈α
we␈α
could␈α
have␈αsentences
␈↓ α∧␈↓like

␈↓ α∧␈↓␈↓ αT␈↓↓∀x.(f(x) = IF f(x) = ␈↓πT␈↓↓ THEN T ELSE ␈↓πT␈↓↓)␈↓

␈↓ α∧␈↓which are self-contradictory.  The version using extended conditional expressions, namely

␈↓ α∧␈↓␈↓ αT␈↓↓∀x.(f(x) = ␈↓αif␈↓↓ f(x) equal ␈↓πT␈↓↓ ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ ␈↓πT␈↓↓)␈↓

␈↓ α∧␈↓is␈αsatisfied␈αby␈α␈↓↓f(x)␈α=␈α␈↓πT␈↓↓␈↓␈αand␈αis␈αtherefore␈αharmless.␈α (Actually␈αextended␈αconditional␈αexpressions␈αcan
␈↓ α∧␈↓be used when we can guarantee that the propositional part is total).

␈↓ α∧␈↓␈↓ αTThe␈α⊂minimal␈α⊂solution␈α⊂is␈α⊂minimal␈α⊂in␈α⊂the␈α⊃sense␈α⊂that␈α⊂any␈α⊂other␈α⊂solution␈α⊂is␈α⊂greater␈α⊃in␈α⊂the
␈↓ α∧␈↓ordering␈αof␈αfunctions␈αpreviously␈αgiven,␈αi.e.␈αif␈α␈↓↓f␈↓␈αis␈αthe␈αminimal␈αsolution␈αand␈α␈↓	f␈↓␈αis␈αanother␈αsolution,
␈↓ α∧␈↓then

␈↓ α∧␈↓20)␈↓ αt ␈↓↓∀x y.(f(x,y) ␈↓πb␈↓↓ ␈↓	f␈↓↓(x,y))␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f12


␈↓ α∧␈↓␈↓ αTThe minimal solution of the functional equation




␈↓ α∧␈↓α6. Axioms for S-expressions, Lists and Integers.

␈↓ α∧␈↓S1: ␈↓↓(∀x y)(issexp x ∧ issexp y ⊃ ispair[x.y] ∧ ␈↓αa␈↓↓[x.y] = x ∧ ␈↓αd␈↓↓[x.y] = y)␈↓

␈↓ α∧␈↓S2: ␈↓↓(∀x)(ispair x ≡ issexp x ∧ ¬␈↓αa␈↓↓t x)␈↓

␈↓ α∧␈↓S3: ␈↓↓(∀x)(ispair x ⊃ issexp ␈↓αa␈↓↓ x ∧ issexp ␈↓αd␈↓↓ x ∧ x = ␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x)␈↓

␈↓ α∧␈↓S4: ␈↓↓(∀u)(islist u ⊃ issexp u)␈↓

␈↓ α∧␈↓S5: ␈↓↓(∀x u)(issexp x ∧ islist u ⊃ islist[x.u])␈↓

␈↓ α∧␈↓S6: ␈↓↓(∀ u)(islist u ∧ ␈↓αa␈↓↓t u ≡ u = ␈↓NIL␈↓↓)␈↓

␈↓ α∧␈↓S7: ␈↓↓(∀x)(issexp x ∧ ␈↓αa␈↓↓t x ⊃ ␈↓	F␈↓↓ x) ∧ (∀x)(ispair x ∧ ␈↓	F␈↓↓ ␈↓αa␈↓↓ x ∧ ␈↓	F␈↓↓ ␈↓αd␈↓↓ x ⊃ ␈↓	F␈↓↓ x) ⊃ (∀x)(issexp x ⊃ ␈↓	F␈↓↓ x)␈↓

␈↓ α∧␈↓S8: ␈↓↓␈↓	F␈↓↓ ␈↓NIL␈↓↓ ∧ (∀u)(islist u ∧ ¬␈↓αn␈↓↓ u ∧ ␈↓	F␈↓↓ ␈↓αd␈↓↓ u ⊃ ␈↓	F␈↓↓ u) ⊃ (∀u)(islist u ⊃ ␈↓	F␈↓↓ u)␈↓




␈↓ α∧␈↓α7. The Functional Equation of a Recursive Program - Applications.




␈↓ α∧␈↓α8. An Extended Example.

␈↓ α∧␈↓␈↓ αTThe␈αSAMEFRINGE␈αproblem␈αis␈αto␈αwrite␈αa␈αprogram␈αthat␈αefficiently␈αdetermines␈αwhether␈αtwo
␈↓ α∧␈↓S-expressions␈α∞have␈α∞the␈α
same␈α∞fringe,␈α∞i.e.␈α
have␈α∞the␈α∞same␈α
atoms␈α∞in␈α∞the␈α
same␈α∞order.␈α∞ (Some␈α
people
␈↓ α∧␈↓omit␈αthe␈αNILs␈αat␈αthe␈αends␈αof␈αlists,␈αbut␈α
we␈αwill␈αtake␈αall␈αatoms).␈α Thus␈α((A.B).C)␈αand␈α(A.(B.C))␈α
have
␈↓ α∧␈↓the␈αsame␈αfringe,␈αnamely␈α(A␈αB␈αC).␈α The␈αobject␈αof␈αthe␈αoriginal␈αproblem␈αwas␈αto␈αprogram␈αit␈αusing␈αa
␈↓ α∧␈↓minimum␈α
of␈α
storage,␈αand␈α
it␈α
was␈αconjectured␈α
that␈α
co-routines␈αwere␈α
necessary␈α
to␈αdo␈α
it␈α
neatly.␈α We
␈↓ α∧␈↓shall not discuss that matter here - merely the extensional correctness of one proposed solution.

␈↓ α∧␈↓␈↓ αTThe relevant recursive definitions are

␈↓ α∧␈↓21)␈↓ αt ␈↓↓fringe x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓,

␈↓ α∧␈↓where ␈↓↓u * v␈↓ denotes the result of appending the lists ␈↓↓u␈↓ and ␈↓↓v␈↓ and is defined recursively by

␈↓ α∧␈↓22)␈↓ αt ␈↓↓u * v ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓.

␈↓ α∧␈↓We are interested in the condition ␈↓↓fringe x = fringe y␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f13


␈↓ α∧␈↓␈↓ αTThe function to be proved correct is ␈↓↓samefringe[x,y]␈↓ defined by the simultaneous recursion

␈↓ α∧␈↓23)␈↓ αt ␈↓↓samefringe[x, y] ← (x = y) ∨ [¬␈↓αa␈↓↓t x ∧ ¬␈↓αa␈↓↓t y ∧ same[gopher x, gopher y]]␈↓,

␈↓ α∧␈↓24)␈↓ αt ␈↓↓same[x, y] ← (␈↓αa␈↓↓ x = ␈↓αa␈↓↓ y) ∧ samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,

␈↓ α∧␈↓where

␈↓ α∧␈↓25)␈↓ αt ␈↓↓gopher x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ gopher ␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x]␈↓.

␈↓ α∧␈↓␈↓ αTWe need to prove that ␈↓↓samefringe␈↓ is total and

␈↓ α∧␈↓26)␈↓ αt ␈↓↓∀xy.(samefringe[x,y] ≡ fringe x = fringe y)␈↓.

␈↓ α∧␈↓␈↓ αTThe␈αminimization␈α
schemata␈αof␈α
these␈αfunctions␈α
are␈αirrelevant,␈α
because␈αwe␈α
will␈αprove␈αthat␈α
the
␈↓ α∧␈↓functions␈αare␈αall␈αtotal␈αexcept␈αthat␈αwe␈αwon't␈αprove␈αanything␈αabout␈αthe␈αresult␈αof␈αapplying␈α␈↓↓gopher␈↓␈αto
␈↓ α∧␈↓an atom.  The functional equations are

␈↓ α∧␈↓27)␈↓ αt ␈↓↓∀x.(fringe x = ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓),

␈↓ α∧␈↓28)␈↓ αt ␈↓↓∀u v.(u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v])␈↓.

␈↓ α∧␈↓29)␈↓ αt␈α
␈↓↓∀x␈αy.(samefringe[x,␈α
y]␈α
=␈αx␈α
equal␈α
y␈αor␈α
[not␈αaat␈α
x␈α
and␈αnot␈α
aat␈α
y␈αand␈α
same[gopher␈αx,␈α
gopher
␈↓ α∧␈↓↓y]])␈↓,

␈↓ α∧␈↓30)␈↓ αt ␈↓↓∀x y.(same[x, y] = ␈↓αa␈↓↓ x equal ␈↓αa␈↓↓ y and samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,

␈↓ α∧␈↓31)␈↓ αt ␈↓↓∀x.(gopher x = ␈↓αif␈↓↓ ␈↓αa␈↓↓t ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ gopher ␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x])␈↓.

␈↓ α∧␈↓Note␈α∞that␈α
because␈α∞␈↓↓samefringe␈↓␈α
and␈α∞␈↓↓same␈↓␈α
are␈α∞recursively␈α
defined␈α∞predicates␈α
which␈α∞have␈α∞not␈α
been
␈↓ α∧␈↓proved␈α
total,␈α
their␈α
functional␈α
equations␈α
must␈α
use␈α
the␈α
imitation␈α
propositional␈α∞functions␈α
involving
␈↓ α∧␈↓the extended truth values.

␈↓ α∧␈↓␈↓ αTWe␈αshall␈αnot␈α
give␈αfull␈αproofs␈αbut␈α
merely␈αthe␈αinduction␈αpredicates␈α
and␈αa␈αfew␈α
indications␈αof
␈↓ α∧␈↓the algebraic transformations.  We begin with a lemma about ␈↓↓gopher␈↓.

␈↓ α∧␈↓32)␈↓ αt ␈↓↓∀x y.(issexp gopher[x.y] ∧ ␈↓αa␈↓↓t ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓.

␈↓ α∧␈↓␈↓ αTThis lemma can be proved by S-expression structural induction using the predicate

␈↓ α∧␈↓33)␈↓ αt ␈↓↓P(x) ≡ ∀y.ok(x,y)␈↓,

␈↓ α∧␈↓where ␈↓↓ok(x,y)␈↓ is defined by

␈↓ α∧␈↓34)␈↓ αt␈↓↓∀x y.(ok(x,y) ≡ issexp gopher[x.y] ∧ ␈↓αa␈↓↓t ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓.

␈↓ α∧␈↓In␈α#the␈α#course␈α"of␈α#the␈α#proof,␈α#we␈α"use␈α#the␈α#associativity␈α"of␈α#*␈α#and␈α#the␈α"formula
␈↓ α∧␈↓␈↓↓fringe[x.y] = fringe x * fringe y␈↓.␈α
 The␈α
lemma␈α
was␈α
expressed␈α
using␈α
␈↓↓gopher[x.y]␈↓␈α
in␈α
order␈α∞to␈α
avoid
␈↓ α∧␈↓considering␈α
atomic␈αarguments␈α
for␈α␈↓↓gopher␈↓,␈α
but␈αit␈α
could␈α
have␈αequally␈α
well␈αbe␈α
proved␈αabout␈α
␈↓↓gopher x␈↓
␈↓ α∧␈↓with the condition ␈↓↓¬␈↓αa␈↓↓t x␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f14


␈↓ α∧␈↓␈↓ αTAnother␈αproof␈αcan␈αbe␈αgiven␈αusing␈αthe␈αcourse-of-values␈αinduction␈αschema␈αfor␈αintegers.␈α We
␈↓ α∧␈↓write this schema

␈↓ α∧␈↓ICV: ␈↓↓∀n.(∀m.(m < n ⊃ P(m)) ⊃ P(n)) ⊃ ∀n.P(n)␈↓,

␈↓ α∧␈↓where␈α␈↓↓m␈↓␈αand␈α␈↓↓n␈↓␈α
range␈αover␈αnon-negative␈αintegers.␈α
 Exactly␈αthe␈αsame␈αschema␈α
expresses␈αtransfinite
␈↓ α∧␈↓induction;␈αwe␈α
need␈αonly␈α
imagine␈αthe␈αvariables␈α
ranging␈αover␈α
all␈αordinals␈αless␈α
than␈αa␈α
given␈αone␈α-␈α
in
␈↓ α∧␈↓this case ␈↓	w␈↓, but equally well ␈↓	w␈↓#
w␈↓#␈↓ or ε␈↓β0␈↓.  We also use the function ␈↓↓size x␈↓ defined by

␈↓ α∧␈↓35)␈↓ αt ␈↓↓size x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ size ␈↓αa␈↓↓ x + size ␈↓αd␈↓↓ x␈↓

␈↓ α∧␈↓satisfying the obvious functional equation.  Our induction predicate is then

␈↓ α∧␈↓36)␈↓ αt ␈↓↓P(n) ≡ ∀x y.(size x = n ⊃ ok(x,y))␈↓.

␈↓ α∧␈↓␈↓ αTFor our proof about ␈↓↓samefringe␈↓ we need one more lemma about ␈↓↓gopher␈↓, namely

␈↓ α∧␈↓37)␈↓ αt ␈↓↓∀x y.(size gopher[x.y] = size[x.y]␈↓.

␈↓ α∧␈↓␈↓ αTThis␈α→can␈α_be␈α→proved␈α→by␈α_either␈α→of␈α_the␈α→above␈α→inductive␈α_methods␈α→or␈α→by␈α_including
␈↓ α∧␈↓␈↓↓size gopher[x.y] = size[x.y]␈↓ in the induction hypothesis ␈↓↓ok[x,y]␈↓.

␈↓ α∧␈↓␈↓ αTThe statement about samefringe is

␈↓ α∧␈↓38)␈↓ αt ␈↓↓∀x y.(issexp samefringe[x,y] ∧ samefringe[x,y] = T ≡ fringe x = fringe y)␈↓,

␈↓ α∧␈↓and it is most easily proved by induction on ␈↓↓size x + size y␈↓ using the predicate

␈↓ α∧␈↓39)␈↓ αt␈α␈↓↓P(n)␈α≡␈α
∀x␈αy.(n␈α=␈α
size␈αx␈α+␈α
size␈αy␈α⊃␈α
issexp␈αsamefringe[x,y]␈α∧␈α
(samefringe[x,y]␈α=␈αT␈α≡␈α
fringe
␈↓ α∧␈↓↓x = fringe y))␈↓.

␈↓ α∧␈↓It␈α
can␈αalso␈α
be␈αproved␈α
using␈α
the␈αwell-foundedness␈α
of␈αlexicographic␈α
ordering␈α
of␈αthe␈α
list␈α␈↓↓<x␈α
␈↓αa␈↓↓␈αx>␈↓,␈α
but
␈↓ α∧␈↓then we must decide what lexicographic orderings to include in our axiom system.

␈↓ α∧␈↓␈↓ αTTransfinite␈α
induction␈α
is␈α∞also␈α
useful,␈α
and␈α∞can␈α
be␈α
illustrated␈α∞with␈α
a␈α
variant␈α∞␈↓↓samefringe␈↓␈α
that
␈↓ α∧␈↓does everything in one complicated recursive definition, namely

␈↓ α∧␈↓40)␈↓ αt␈α␈↓↓samefringe[x,y]␈α=␈α(x␈αequal␈αy)␈αor␈αnot␈αaat␈αx␈αand␈α
not␈αaat␈αy␈αand␈α[␈↓αif␈↓↓␈α␈↓αa␈↓↓t␈α␈↓αa␈↓↓␈αx␈α␈↓αthen␈↓↓␈α[␈↓αif␈↓↓␈α␈↓αa␈↓↓t␈αy␈α
␈↓αthen␈↓↓
␈↓ α∧␈↓↓␈↓αa␈↓↓␈α
x␈α
equal␈α
␈↓αa␈↓↓␈α
y␈α
and␈α
samefringe[␈↓αd␈↓↓␈α
x,␈α
␈↓αd␈↓↓␈α
y]␈α
␈↓αelse␈↓↓␈α
samefringe[x,␈α
␈↓αaa␈↓↓␈α
y␈α
.␈α
[␈↓αda␈↓↓␈α
y␈α
.␈α
␈↓αd␈↓↓␈α
y]]]␈α
␈↓αelse␈↓↓␈αsamefringe[␈↓αaa␈↓↓␈α
x
␈↓ α∧␈↓↓. [␈↓αda␈↓↓ x .␈↓αd␈↓↓ x], y]␈↓.

␈↓ α∧␈↓The transfinite induction predicate then has the form

␈↓ α∧␈↓41)␈↓ αt␈α∞␈↓↓P(n)␈α∂≡␈α∞∀x␈α∞y.[n␈α∂=␈α∞␈↓	w␈↓↓(size␈α∞x␈α∂+␈α∞size␈α∂y)␈α∞+␈α∞size␈α∂␈↓αa␈↓↓␈α∞x␈α∞+␈α∂size␈α∞␈↓αa␈↓↓␈α∞y␈α∂⊃␈α∞issexp␈α∂samefringe[x,y]␈α∞∧
␈↓ α∧␈↓↓(samefringe[x,y] = T ≡ fringe x = fringe y)]␈↓.

␈↓ α∧␈↓␈↓ αTAn␈α
easier␈αexample␈α
requiring␈α
induction␈αup␈α
to␈α␈↓	w␈↓∧2␈↓␈α
is␈α
proving␈αthe␈α
termination␈αof␈α
Ackermann's
␈↓ α∧␈↓function which has the functional equation

␈↓ α∧␈↓42)␈↓ αt ␈↓↓∀m n.(A(m,n) = ␈↓αif␈↓↓ m = 0 ␈↓αthen␈↓↓ n+1 ␈↓αelse␈↓↓ ␈↓αif␈↓↓ n = 0 ␈↓αthen␈↓↓ A(m-1,0) ␈↓αelse␈↓↓ A(m-1,A(m,n-1)))␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f15


␈↓ α∧␈↓The statement to be proved is

␈↓ α∧␈↓43)␈↓ αt ␈↓↓∀α.(α < ␈↓	w␈↓∧2␈↓↓ ∧ α = ␈↓	w␈↓↓m + n ⊃ isint A(m,n))␈↓.

␈↓ α∧␈↓The␈α
proof␈α
is␈αstraightforward,␈α
because␈α
␈↓	w␈↓↓(m-1) < ␈↓	w␈↓↓m+n␈↓␈α
and␈α␈↓	w␈↓↓m+(n-1) < ␈↓	w␈↓↓m+n␈↓,␈α
so␈α
we␈αcan␈α
assume
␈↓ α∧␈↓␈↓↓isint A(m-1,0)␈↓␈α∞and␈α∂␈↓↓isint A(m,n-1)␈↓.␈α∞ From␈α∞the␈α∂latter,␈α∞it␈α∞follows␈α∂that␈α∞␈↓	w␈↓↓(m-1)+A(m,n-1) < ␈↓	w␈↓↓m+n␈↓
␈↓ α∧␈↓which completes the induction step.

␈↓ α∧␈↓␈↓ αTWe␈α↔would␈α↔like␈α↔to␈α↔prove␈α↔that␈α↔the␈α↔amount␈α↔of␈α↔storage␈α↔used␈α↔in␈α↔the␈α↔computation␈α⊗of
␈↓ α∧␈↓␈↓↓samefringe[x,y]␈↓␈αaside␈α
from␈αthat␈αoccupied␈α
by␈α␈↓↓x␈↓␈α
and␈α␈↓↓y,␈↓␈αnever␈α
exceeds␈αthe␈αsum␈α
of␈αthe␈α
numbers␈αof
␈↓ α∧␈↓␈↓↓car␈↓s␈αrequired␈αto␈αreach␈αcorresponding␈αatoms␈αin␈α␈↓↓x␈↓␈αand␈α␈↓↓y.␈↓␈αUnfortunately,␈αwe␈αcan't␈αeven␈αexpress␈αthat
␈↓ α∧␈↓fact,␈αbecause␈αwe␈α
are␈αaxiomatizing␈αthe␈αprograms␈α
as␈αfunctions,␈αand␈αthe␈α
amount␈αof␈αstorage␈αused␈α
does
␈↓ α∧␈↓not␈α∞depend␈α∞merely␈α∞on␈α∂the␈α∞function␈α∞being␈α∞computed;␈α∞it␈α∂depends␈α∞on␈α∞the␈α∞method␈α∂of␈α∞computation.
␈↓ α∧␈↓We␈αmay␈α
regard␈αsuch␈αthings␈α
as␈α␈↓↓intensional␈↓␈αproperties,␈α
but␈αany␈αcorrespondence␈α
with␈αthe␈α
notion␈αof
␈↓ α∧␈↓intensional properties in intensional logic remains to be established.


␈↓ α∧␈↓α9. The Minimization Schema.

␈↓ α∧␈↓␈↓ αTThe␈αfunctional␈αequation␈α
of␈αa␈αprogram␈αdoesn't␈α
completely␈αcharacterize␈αit.␈α For␈α
example,␈αthe
␈↓ α∧␈↓program

␈↓ α∧␈↓44)␈↓ αt ␈↓↓f1 x ← f1 x␈↓

␈↓ α∧␈↓leads to the sentence

␈↓ α∧␈↓45)␈↓ αt ␈↓↓∀x.(f1 x = f1 x)␈↓

␈↓ α∧␈↓which␈αprovides␈αno␈αinformation␈αalthough␈αthe␈αfunction␈α␈↓↓f␈↓␈αis␈αundefined␈αfor␈αall␈α␈↓↓x.␈↓␈αThis␈αis␈αnot␈αalways
␈↓ α∧␈↓the case, since the program

␈↓ α∧␈↓46)␈↓ αt ␈↓↓f2 x ← (f2 x).␈↓NIL␈↓↓␈↓

␈↓ α∧␈↓has the functional equation

␈↓ α∧␈↓47)␈↓ αt ␈↓↓∀x.(f2 x = (f2 x).␈↓NIL␈↓↓)␈↓.

␈↓ α∧␈↓from which ␈↓↓∀x.¬issexp f2(x)␈↓ can be proved by induction.

␈↓ α∧␈↓␈↓ αTIn␈α⊃order␈α⊂to␈α⊃characterize␈α⊃recursive␈α⊂programs,␈α⊃we␈α⊃need␈α⊂some␈α⊃way␈α⊃of␈α⊂asking␈α⊃for␈α⊃the␈α⊂least
␈↓ α∧␈↓defined solution of the functional equation.

␈↓ α∧␈↓␈↓ αTSuppose the program is

␈↓ α∧␈↓48)␈↓ αt ␈↓↓f x ← ␈↓	t␈↓↓[f](x)␈↓

␈↓ α∧␈↓yielding the functional equation

␈↓ α∧␈↓49)␈↓ αt ␈↓↓∀x.(f x = ␈↓	t␈↓↓[f](x)␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f16


␈↓ α∧␈↓The ␈↓↓minimization schema␈↓ is then

␈↓ α∧␈↓50)␈↓ αt ␈↓↓∀x.(isD ␈↓	t␈↓↓[␈↓	f␈↓↓](x) ⊃ ␈↓	f␈↓↓ x = ␈↓	t␈↓↓[␈↓	f␈↓↓](x)) ⊃ ∀x.(isD f x ⊃ ␈↓	f␈↓↓ x = f x)␈↓,

␈↓ α∧␈↓where the predicate ␈↓↓isD␈↓ asserts that its argument is in the domain ␈↓↓D␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α∞␈↓↓minimization␈α
schema␈↓␈α∞can␈α
be␈α∞abbreviated␈α
by␈α∞introducing␈α
Scott's␈α∞partial␈α
ordering␈α∞␈↓πb␈↓␈α
on
␈↓ α∧␈↓D␈↓∧+␈↓.  We define

␈↓ α∧␈↓51)␈↓ αt␈↓↓∀X Y.(X ␈↓πb␈↓↓ Y ≡ X = ␈↓πT␈↓↓ ∨ X = Y)␈↓,

␈↓ α∧␈↓so␈αthat␈αthe␈αonly␈αproper␈αordering␈αis␈αthat␈α␈↓πT␈↓␈αis␈αless␈αthan␈αeverything␈αelse.␈α We␈αalso␈αuse␈αthe␈αsymbol␈α␈↓πd␈↓.
␈↓ α∧␈↓The minimization schema then becomes

␈↓ α∧␈↓52)␈↓ αt ␈↓↓∀x.(␈↓	t␈↓↓[␈↓	f␈↓↓](x) ␈↓πb␈↓↓ ␈↓	f␈↓↓(x)) ⊃ ∀x.(f(x) ␈↓πb␈↓↓ ␈↓	f␈↓↓(x))␈↓,

␈↓ α∧␈↓which makes it more apparent that the minimization schema asserts that ␈↓↓f␈↓ is minimal.

␈↓ α∧␈↓␈↓ αTIn the ␈↓↓subst␈↓ example, the schema is

␈↓ α∧␈↓53)␈↓ αt␈↓↓∀x␈αy␈α
z.(␈↓	f␈↓↓(x,y,z)␈α␈↓πd␈↓↓␈α
␈↓αif␈↓↓␈α␈↓αa␈↓↓t␈α
z␈α␈↓αthen␈↓↓␈α
(␈↓αif␈↓↓␈αz␈α=␈α
y␈α␈↓αthen␈↓↓␈α
x␈α␈↓αelse␈↓↓␈α
z)␈α␈↓αelse␈↓↓␈α
␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈αz).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α
z))␈α⊃␈α∀x␈α
y
␈↓ α∧␈↓↓z.(␈↓	f␈↓↓(x,y,z) ␈↓πd␈↓↓ subst(x,y,z))␈↓,

␈↓ α∧␈↓which has also the longer form

␈↓ α∧␈↓54)␈↓ αt␈α⊂␈↓↓∀x␈α⊂y␈α⊂z.(issexp␈α⊂(␈↓αif␈↓↓␈α⊂␈↓αa␈↓↓t␈α⊂z␈α⊂␈↓αthen␈↓↓␈α⊂(␈↓αif␈↓↓␈α⊂z␈α⊂=␈α⊂y␈α⊂␈↓αthen␈↓↓␈α⊂x␈α⊂␈↓αelse␈↓↓␈α⊂z)␈α⊂␈↓αelse␈↓↓␈α⊂␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α⊂z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α⊂z))␈α⊂⊃
␈↓ α∧␈↓↓(␈↓	f␈↓↓(x,y,z)␈α∞=␈α∞␈↓αif␈↓↓␈α∞␈↓αa␈↓↓t␈α∞z␈α∞␈↓αthen␈↓↓␈α∞(␈↓αif␈↓↓␈α∞z␈α∞=␈α∞y␈α∞␈↓αthen␈↓↓␈α∞x␈α∞␈↓αelse␈↓↓␈α∞z)␈α∞␈↓αelse␈↓↓␈α∞␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α∞z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α∞z)))␈α∞⊃␈α∞∀x␈α∞y␈α∞z.(issexp
␈↓ α∧␈↓↓subst(x,y,z) ⊃ ␈↓	f␈↓↓(x,y,z) = subst(x,y,z))␈↓.

␈↓ α∧␈↓␈↓ αTIn␈αthe␈αschema␈α␈↓	f␈↓␈αis␈αa␈αfree␈αfunction␈αvariable␈αof␈αthe␈αappropriate␈αnumber␈αof␈αarguments.␈α The
␈↓ α∧␈↓schema is just a translation into first order logic of Park's (1970) theorem

␈↓ α∧␈↓55)␈↓ αt ␈↓↓␈↓	f␈↓↓ ␈↓πd␈↓↓ ␈↓	t␈↓↓[␈↓	f␈↓↓] ⊃ ␈↓	f␈↓↓ ␈↓πd␈↓↓ Y[␈↓	t␈↓↓]␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α
simplest␈α
application␈α
of␈αthe␈α
schema␈α
is␈α
to␈αshow␈α
that␈α
the␈α
␈↓↓f1␈↓␈α
defined␈αby␈α
(44)␈α
is␈α
never␈αan␈α
S-
␈↓ α∧␈↓expression.  The schema becomes

␈↓ α∧␈↓56)␈↓ αt ␈↓↓∀x.(␈↓	f␈↓↓ x ␈↓πd␈↓↓ ␈↓	f␈↓↓ x) ⊃ ∀x.(␈↓	f␈↓↓ x ␈↓πd␈↓↓ f1 x)␈↓,

␈↓ α∧␈↓and we take

␈↓ α∧␈↓57)␈↓ αt ␈↓↓␈↓	f␈↓↓ x = ␈↓πT␈↓↓␈↓.

␈↓ α∧␈↓The␈αleft␈αside␈αof␈α(56)␈αis␈αidentically␈αtrue,␈αand,␈αremembering␈αthat␈α␈↓πT␈↓␈αis␈αnot␈αan␈αS-expression,␈αthe␈αright
␈↓ α∧␈↓side tells us that ␈↓↓f1 x␈↓ is never an S-expression.

␈↓ α∧␈↓␈↓ αTThe␈αminimization␈αschema␈αcan␈αsometimes␈αbe␈αused␈αto␈αshow␈αpartial␈αcorrectness.␈α For␈αexample,
␈↓ α∧␈↓the well known 91-function is defined by the recursive program over the integers

␈↓ α∧␈↓58)␈↓ αt ␈↓↓f91 x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ f91 f91(x + 11)␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f17


␈↓ α∧␈↓The goal is to show that

␈↓ α∧␈↓59)␈↓ αt ␈↓↓∀x.(f91 x = ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ 91)␈↓.

␈↓ α∧␈↓We apply the minimization schema with

␈↓ α∧␈↓60)␈↓ αt ␈↓↓␈↓	f␈↓↓ x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ 91␈↓,

␈↓ α∧␈↓and␈α
it␈αcan␈α
be␈α
shown␈αby␈α
an␈α
explicit␈αcalculation␈α
without␈α
induction␈αthat␈α
the␈α
premiss␈αof␈α
the␈αschema␈α
is
␈↓ α∧␈↓satisfied, and this shows that ␈↓↓f91,␈↓ whenever defined has the desired value.

␈↓ α∧␈↓␈↓ αTThe␈α
method␈α
of␈α
recursion␈α
induction␈α
(McCarthy␈α1963)␈α
is␈α
also␈α
an␈α
immediate␈α
application␈αof␈α
the
␈↓ α∧␈↓minimization␈α
schema.␈α
 If␈α
we␈α
show␈α
that␈α
two␈αfunctions␈α
satisfy␈α
the␈α
schema␈α
of␈α
a␈α
recursive␈αprogram,
␈↓ α∧␈↓we␈α
show␈α
that␈αthey␈α
both␈α
equal␈α
the␈αfunction␈α
computed␈α
by␈α
the␈αprogram␈α
on␈α
whereever␈α
the␈αfunction␈α
is
␈↓ α∧␈↓defined.

␈↓ α∧␈↓␈↓ αTThe␈α
utility␈α
of␈α
the␈α
minimization␈αschema␈α
for␈α
proving␈α
partial␈α
correctness␈α
or␈αnon-termination
␈↓ α∧␈↓depends␈α∂on␈α∂our␈α∞ability␈α∂to␈α∂name␈α∂suitable␈α∞comparison␈α∂functions.␈α∂ f1␈α∞and␈α∂f91␈α∂were␈α∂easily␈α∞treated,
␈↓ α∧␈↓because␈α⊃the␈α⊃necessary␈α⊃comparison␈α⊃functions␈α⊃could␈α⊃be␈α⊃given␈α⊃explicitly␈α⊃without␈α⊃recursion.␈α⊂ Any
␈↓ α∧␈↓extension␈αof␈αthe␈αlanguage␈αthat␈αprovides␈αnew␈αtools␈αfor␈αnaming␈αcomparison␈αfunctions,␈αe.g.␈αgoing␈αto
␈↓ α∧␈↓higher order logic, will improve our ability to use the schema in proofs.

␈↓ α∧␈↓␈↓ αT(50)␈α∞can␈α∞be␈α∂regarded␈α∞as␈α∞an␈α∂axiom␈α∞schema␈α∞involving␈α∞a␈α∂second␈α∞order␈α∞function␈α∂variable␈α∞␈↓	t␈↓.
␈↓ α∧␈↓What␈αcan␈αbe␈αsubstituted␈αfor␈α␈↓	t␈↓␈αis␈αa␈αquantifier␈αfree␈αλ-expression␈αin␈αa␈αfirst␈αorder␈αfunction␈αvariable.
␈↓ α∧␈↓It␈α
may␈α
be␈α
interesting␈α
to␈α
study␈α
the␈α
sets␈α
of␈α
first␈α
order␈α
sentences␈α
that␈α
can␈α
be␈α
generated␈α
by␈αsuch␈α
second
␈↓ α∧␈↓order␈αsentence␈αschemata.␈α Presumably,␈αsets␈αof␈αsentences␈αcan␈αbe␈αgenerated␈αin␈αthis␈αway␈αthat␈αcannnot
␈↓ α∧␈↓be generated by schemata with only first order function variables.



␈↓ α∧␈↓α10. Proof Methods as Axiom Schemata

␈↓ α∧␈↓␈↓ αTRepresenting␈α
recursive␈α
definitions␈α
in␈αfirst␈α
order␈α
logic␈α
permits␈αus␈α
to␈α
express␈α
some␈αwell␈α
known
␈↓ α∧␈↓methods for proving partial correctness as axiom schemata of first order logic.

␈↓ α∧␈↓␈↓ αTFor example, suppose we want to prove that if the input ␈↓↓x␈↓ of a function ␈↓↓f␈↓ defined by

␈↓ α∧␈↓61)␈↓ αt ␈↓↓f x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ f h x␈↓

␈↓ α∧␈↓satisfies␈α␈↓↓␈↓	F␈↓↓(x)␈↓,␈αthen␈αif␈αthe␈αfunction␈αterminates,␈αthe␈αoutput␈α␈↓↓f(x)␈↓␈αwill␈αsatisfy␈α␈↓	Y␈↓↓(x,f(x))␈↓.␈α We␈αappeal␈αto
␈↓ α∧␈↓the following ␈↓↓axiom schema of inductive assertions␈↓:

␈↓ α∧␈↓62)␈↓ αt ␈↓↓∀x.(␈↓	F␈↓↓(x) ⊃ q(x,x)) ∧ ∀x y.(q(x,y) ⊃ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ ␈↓	Y␈↓↓(x,y) ␈↓αelse␈↓↓ q(x,␈↓π ␈↓↓h y))
␈↓ α∧␈↓↓                ⊃ ∀x.(␈↓	F␈↓↓(x) ∧ isD f x ⊃ ␈↓	Y␈↓↓(x,f x))␈↓


␈↓ α∧␈↓where␈α␈↓↓isD␈α
f␈αx␈↓␈α
is␈αthe␈α
assertion␈αthat␈α
␈↓↓f(x)␈↓␈αis␈α
in␈αthe␈α
nominal␈αrange␈α
of␈αthe␈α
function␈αdefinition,␈α
i.e.␈αis␈α
an
␈↓ α∧␈↓integer␈α∞or␈α
an␈α∞S-expression␈α∞as␈α
the␈α∞case␈α
may␈α∞be,␈α∞and␈α
asserts␈α∞that␈α
the␈α∞computation␈α∞terminates.␈α
 In
␈↓ α∧␈↓order␈α⊂to␈α⊂use␈α⊂the␈α∂schema,␈α⊂we␈α⊂must␈α⊂invent␈α∂a␈α⊂suitable␈α⊂predicate␈α⊂␈↓↓q(x,y)␈↓,␈α∂and␈α⊂this␈α⊂is␈α⊂precisely␈α∂the
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f18


␈↓ α∧␈↓method␈αof␈αinductive␈αassertions.␈α The␈αschema␈αis␈αvalid␈αfor␈αall␈αpredicates␈α␈↓	F␈↓,␈α␈↓	Y␈↓,␈αand␈α␈↓↓q␈↓,␈αand␈αa␈αsimilar
␈↓ α∧␈↓schema can be written for any collection of mutually recursive definitions that is iterative.

␈↓ α∧␈↓␈↓ αTThe␈α∂method␈α∂of␈α∞␈↓↓subgoal␈α∂induction␈↓␈α∂for␈α∞recursive␈α∂programs␈α∂was␈α∞introduced␈α∂in␈α∂(Manna␈α∞and
␈↓ α∧␈↓Pnueli␈α∂1970),␈α⊂but␈α∂they␈α∂didn't␈α⊂give␈α∂it␈α⊂a␈α∂name.␈α∂ Morris␈α⊂and␈α∂Wegbreit␈α∂(1977)␈α⊂name␈α∂it,␈α⊂extend␈α∂it
␈↓ α∧␈↓somewhat,␈α⊂and␈α⊂apply␈α⊂it␈α∂to␈α⊂Algol-like␈α⊂programs.␈α⊂ Unlike␈α∂␈↓↓inductive␈α⊂assertions␈↓,␈α⊂it␈α⊂isn't␈α⊂limited␈α∂to
␈↓ α∧␈↓iterative definitions.  Thus, for the recursive program

␈↓ α∧␈↓63)␈↓ αt ␈↓↓f␈↓β5␈↓↓ x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f␈↓β5␈↓↓ g2 x␈↓,

␈↓ α∧␈↓where ␈↓↓p␈↓ is assumed total, we have

␈↓ α∧␈↓64)␈↓ αt ␈↓↓∀x.(p x ⊃ q(x,h x)) ∧ ∀x z.(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧ ∀x.(␈↓	F␈↓↓(x) ∧ q(x,z) ⊃ ␈↓	Y␈↓↓(x,z))
␈↓ α∧␈↓↓                ⊃ ∀x.(␈↓	F␈↓↓(x) ∧ isD(f(x)) ⊃ ␈↓	Y␈↓↓(x,f(x)))␈↓

␈↓ α∧␈↓␈↓ αTWe␈α∞can␈α∞express␈α∞these␈α∞methods␈α∞as␈α∂axiom␈α∞schemata,␈α∞because␈α∞we␈α∞have␈α∞the␈α∞predicate␈α∂␈↓↓isD␈↓␈α∞to
␈↓ α∧␈↓express␈α∞termination.␈α∞ The␈α∞minimization␈α∞schema␈α∞itself␈α∞can␈α∞be␈α∞proved␈α∞by␈α∞subgoal␈α∞induction.␈α
 We
␈↓ α∧␈↓need only take ␈↓↓␈↓	F␈↓↓(x) ≡ ␈↓αtrue␈↓ and ␈↓	Y␈↓↓(x,y) ≡ (y = ␈↓	f␈↓↓(x))␈↓ and ␈↓↓q(x,y) ≡ (y = ␈↓	f␈↓↓(x))␈↓.

␈↓ α∧␈↓␈↓ αTGeneral␈α
rules␈αfor␈α
going␈αfrom␈α
a␈αrecursive␈α
program␈α
to␈αwhat␈α
amounts␈αto␈α
the␈αsubgoal␈α
induction
␈↓ α∧␈↓schema␈α
are␈α
given␈α
in␈α
(Manna␈α
and␈α
Pnueli␈α
1970)␈α
and␈α
(Morris␈α
and␈α
Wegbreit␈α
1977);␈α
we␈α
need␈α
only␈α
add
␈↓ α∧␈↓a conclusion involving the ␈↓↓isD␈↓ predicate to the Manna's and Pnueli formula ␈↓↓W␈↓βP␈↓.

␈↓ α∧␈↓␈↓ αTHowever,␈α∞we␈α
can␈α∞characterize␈α
subgoal␈α∞induction␈α
as␈α∞an␈α
axiom␈α∞schema.␈α
 Namely,␈α∞we␈α
define
␈↓ α∧␈↓␈↓	t␈↓↓'[q]␈↓ as an extension of ␈↓	t␈↓ mapping relations into relations.  Thus if

␈↓ α∧␈↓65)␈↓ αt ␈↓↓␈↓	t␈↓↓[f](x) = ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f g2 x␈↓,

␈↓ α∧␈↓we have

␈↓ α∧␈↓66)␈↓ αt ␈↓↓␈↓	t␈↓↓'[q](x,y) ≡ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ (y = h x) ␈↓αelse␈↓↓ ∃z.(q(g2 x,z) ∧ y = g1 z)␈↓.

␈↓ α∧␈↓In general we have

␈↓ α∧␈↓67)␈↓ αt ␈↓↓∀xy.(␈↓	t␈↓↓'[q](x,y) ⊃ q(x,y)) ⊃ ∀x.(isD f x ⊃ q(x,f x))␈↓,

␈↓ α∧␈↓from␈α
which␈α
the␈α
subgoal␈α
induction␈α
rule␈α
follows␈α∞immediately␈α
given␈α
the␈α
properties␈α
of␈α
␈↓	F␈↓␈α
and␈α∞␈↓	Y␈↓.␈α
 I
␈↓ α∧␈↓am indebted to Wolfgang Polak (oral communication) for help in elucidating this relationship.

␈↓ α∧␈↓␈↓αWARNING␈↓:␈αThe␈αrest␈α
of␈αthis␈αsection␈α
is␈αstill␈αsomewhat␈α
conjectural␈αand␈αis␈α
subject␈αto␈αchange.␈α
 There
␈↓ α∧␈↓may be bugs.

␈↓ α∧␈↓␈↓ αTThe␈αextension␈α␈↓↓␈↓	t␈↓↓'[q]␈↓␈α
can␈αbe␈αdetermined␈αas␈α
follows:␈αIntroduce␈αinto␈αthe␈α
logic␈αthe␈αnotion␈α
of␈αa
␈↓ α∧␈↓␈↓↓multi-term␈↓␈α
which␈αis␈α
formed␈αin␈α
the␈αsame␈α
way␈α
as␈αa␈α
term␈αbut␈α
allows␈αrelations␈α
written␈α
as␈αfunctions.
␈↓ α∧␈↓For␈α∀the␈α∀present␈α∃we␈α∀won't␈α∀interpret␈α∃them␈α∀but␈α∀merely␈α∀give␈α∃rules␈α∀for␈α∀introducing␈α∃them␈α∀and
␈↓ α∧␈↓subsequently␈α
eliminating␈αthem␈α
again␈α
to␈αget␈α
an␈α
ordinary␈αformula.␈α
 Thus␈α
we␈αwill␈α
write␈α
␈↓↓q<e>␈↓␈αwhere␈α
␈↓↓e␈↓
␈↓ α∧␈↓is␈αany␈αterm␈αor␈αmulti-term.␈α We␈αthen␈αform␈α␈↓↓␈↓	t␈↓↓'[q]␈↓␈αexactly␈αin␈αthe␈αsame␈αway␈α␈↓↓␈↓	t␈↓↓[f]␈↓␈αwas␈αformed.␈α Thus
␈↓ α∧␈↓for the 91-function we have

␈↓ α∧␈↓68)␈↓ αt ␈↓↓␈↓	t␈↓↓'[q](x) = ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ q<q<x+11>>␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f19


␈↓ α∧␈↓The␈α⊃pointy␈α⊃brackets␈α⊂indicate␈α⊃that␈α⊃we␈α⊂are␈α⊃"applying"␈α⊃a␈α⊂relation.␈α⊃ We␈α⊃now␈α⊃evaluate␈α⊂␈↓↓␈↓	t␈↓↓'[q](x,y)␈↓
␈↓ α∧␈↓formally as follows:

␈↓ α∧␈↓69)␈↓ αt ␈↓↓␈↓	t␈↓↓'[q](x,y) ≡ (␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ q<q<x+11>>)(y)

␈↓ α∧␈↓↓≡ ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ y = x-10 ␈↓αelse␈↓↓ q(q<x+11>,y)

␈↓ α∧␈↓↓≡ ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ y = x-10 ␈↓αelse␈↓↓ ∃z.(q(x+11,z) ∧ q(z,y))␈↓.

␈↓ α∧␈↓This␈α⊂last␈α⊂formula␈α∂has␈α⊂no␈α⊂pointy␈α∂brackets␈α⊂and␈α⊂is␈α∂just␈α⊂the␈α⊂formula␈α∂that␈α⊂would␈α⊂be␈α⊂obtained␈α∂by
␈↓ α∧␈↓Manna and Pnueli or Morris and Wegbreit.  The rules are as follows:

␈↓ α∧␈↓␈↓ αT(i)␈α∂␈↓↓␈↓	t␈↓↓'[q](x)␈↓␈α∞is␈α∂just␈α∞like␈α∂␈↓↓␈↓	t␈↓↓[f](x)␈↓␈α∞except␈α∂that␈α∂␈↓↓q␈↓␈α∞replaces␈α∂␈↓↓f␈↓␈α∞and␈α∂takes␈α∞its␈α∂arguments␈α∂in␈α∞pointy
␈↓ α∧␈↓brackets.

␈↓ α∧␈↓␈↓ αT(ii) an ordinary term ␈↓↓e␈↓ applied to ␈↓↓y␈↓ becomes ␈↓↓y = e␈↓.

␈↓ α∧␈↓␈↓ αT(ii) ␈↓↓q<e>(y)␈↓ becomes ␈↓↓q(e,y)␈↓.

␈↓ α∧␈↓␈↓ αT(ii)␈α∪␈↓↓P(q<e>)␈↓␈α∩becomes␈α∪␈↓↓∃z.q(e,z) ∧ P(z)␈↓␈α∩when␈α∪␈↓↓P(q<e>)␈↓␈α∩occurs␈α∪positively␈α∩in␈α∪␈↓↓␈↓	t␈↓↓'[q](x,y)␈↓␈α∩and
␈↓ α∧␈↓becomes␈α⊂␈↓↓∀z.q(e,z) ⊃ P(z)␈↓␈α⊂when␈α⊂the␈α⊂occurrence␈α⊂is␈α⊂negatve.␈α⊂ It␈α⊂is␈α⊂not␈α⊂evident␈α⊃what␈α⊂independent
␈↓ α∧␈↓semantics should be given to multi-terms.




␈↓ α∧␈↓α11. Representations Using Finite Approximations.

␈↓ α∧␈↓␈↓ αTOur␈αsecond␈αapproach␈αto␈αrepresenting␈αrecursive␈αprograms␈αby␈αfirst␈αorder␈αformulas␈αgoes␈αback
␈↓ α∧␈↓to␈α⊂G␈↓
:␈↓odel␈α⊂(1931,␈α∂1934)␈α⊂who␈α⊂showed␈α∂that␈α⊂primitive␈α⊂recursive␈α∂functions␈α⊂could␈α⊂be␈α⊂so␈α∂represented.
␈↓ α∧␈↓(Our knowledge of G␈↓
:␈↓odel's work comes from (Kleene 1951)).

␈↓ α∧␈↓␈↓ αTKleene␈α(1951)␈α
calls␈αa␈αfunction␈α
␈↓↓f␈↓␈α␈↓↓representable␈↓␈αif␈α
there␈αis␈αan␈α
arithmetic␈αformula␈α␈↓↓A␈↓␈α
with␈αfree
␈↓ α∧␈↓variables ␈↓↓x␈↓ and ␈↓↓y␈↓ such that

␈↓ α∧␈↓1)␈↓ αt ␈↓↓∀x y.((y = f(x)) ≡ A)␈↓,

␈↓ α∧␈↓where␈αan␈αarithmetic␈αformula␈αis␈αbuilt␈αup␈αfrom␈αinteger␈αconstants␈αand␈αvariables␈αusing␈αonly␈αaddition,
␈↓ α∧␈↓multiplication␈αand␈αbounded␈α
quantification.␈α Kleene␈αshowed␈αthat␈α
all␈αpartial␈αrecursive␈αfunctions␈α
are
␈↓ α∧␈↓representable.␈α The␈α
proof␈αinvolves␈αG␈↓
:␈↓odel␈α
numbering␈αpossible␈α
computation␈αsequences␈αand␈α
showing
␈↓ α∧␈↓that␈α
the␈α∞relation␈α
between␈α
sequences␈α∞and␈α
their␈α
elements␈α∞and␈α
the␈α
steps␈α∞of␈α
the␈α
computation␈α∞are␈α
all
␈↓ α∧␈↓representable.

␈↓ α∧␈↓␈↓ αTIn␈αLisp␈αless␈αmachinery␈α
is␈αneeded,␈αbecause␈αsequences␈αare␈α
Lisp␈αdata,␈αand␈αthe␈αrelation␈α
between
␈↓ α∧␈↓a␈αsequence␈αand␈αits␈αelements␈αis␈αgiven␈αby␈αbasic␈αLisp␈αfunctions␈αand␈αby␈αthe␈α␈↓↓occurence␈αrelation␈↓␈αdefined
␈↓ α∧␈↓in section 5 by

␈↓ α∧␈↓2)␈↓ αt ␈↓↓occur[x,y] ← (x = y) ∨ ¬␈↓αa␈↓↓t y ∧ [occur[x,␈↓αa␈↓↓ y] ∨ occur[x, ␈↓αd␈↓↓ y]]␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f20


␈↓ α∧␈↓␈↓ αT␈↓↓occur␈↓␈α∂is␈α∞the␈α∂only␈α∞recursive␈α∂definition␈α∞we␈α∂shall␈α∂require.␈α∞ Since␈α∂it␈α∞is␈α∂total,␈α∞we␈α∂only␈α∂need␈α∞its
␈↓ α∧␈↓functional equation to represent it in first order logic.  The functional equation is

␈↓ α∧␈↓L17: ␈↓↓∀x y.(occur[x,y] ≡ (x=y) ∨ ¬␈↓αa␈↓↓t y ∧ (occur[x,␈↓αa␈↓↓ y] ∨ occur[x,␈↓αd␈↓↓ y]))␈↓,

␈↓ α∧␈↓␈↓ αTThe␈α⊃axiom␈α⊃system␈α⊃consisting␈α⊂of␈α⊃L1-L17,␈α⊃B1-B12,␈α⊃and␈α⊂the␈α⊃sentences␈α⊃resulting␈α⊃from␈α⊂the
␈↓ α∧␈↓schemata LS1 and LS2 will be called the axiom system Lisp1.

␈↓ α∧␈↓␈↓ αTStarting␈α
with␈α
␈↓↓occur␈↓␈α
and␈α
the␈α
basic␈α
Lisp␈αfunctions␈α
and␈α
predicates␈α
we␈α
will␈α
define␈α
three␈αother
␈↓ α∧␈↓Lisp␈α⊃predicates␈α⊂without␈α⊃recursion.␈α⊂ By␈α⊃␈↓↓u istail v␈↓␈α⊂we␈α⊃mean␈α⊂that␈α⊃␈↓↓u␈↓␈α⊂can␈α⊃be␈α⊂obtained␈α⊃from␈α⊃␈↓↓v␈↓␈α⊂by
␈↓ α∧␈↓repeated␈α␈↓↓cdr␈↓s.␈α Thus␈αthe␈αtails␈αof␈α(A␈α
B␈αC␈αD)␈αare␈α(A␈αB␈αC␈αD),␈α
(B␈αC␈αD),␈α(C␈αD),␈α(D)␈αand␈α
NIL.␈α The
␈↓ α∧␈↓natural recursive definition of ␈↓↓istail␈↓ is

␈↓ α∧␈↓3)␈↓ αt ␈↓↓u istail v ← (u = v) ∨ (¬␈↓αn␈↓↓ v ∧ u istail ␈↓αd␈↓↓ v)␈↓

␈↓ α∧␈↓which according to the previous sections would lead to the first order formula

␈↓ α∧␈↓4)␈↓ αt ␈↓↓∀u v.(u istail v ≡ (u = v) ∨ (¬␈↓αn␈↓↓ v ∧ u istail ␈↓αd␈↓↓ v))␈↓,

␈↓ α∧␈↓but␈α
(4)␈α
is␈α
still␈α
an␈αimplicit␈α
definition␈α
of␈α
␈↓↓istail␈↓,␈α
because␈αthe␈α
function␈α
being␈α
defined␈α
occurs␈α
on␈αboth
␈↓ α∧␈↓sides of the equivalence sign.  A suitable explicit definition is

␈↓ α∧␈↓5)␈↓ αt ␈↓↓∀u v.(u istail v ≡ occur[u,v] ∧ ∀x.(occur[u,x] ∧ occur[x,v] ⊃ x = u ∨ occur[u, ␈↓αd␈↓↓ x]))␈↓.

␈↓ α∧␈↓Next we shall define membership in a list.  We have

␈↓ α∧␈↓6)␈↓ αt ␈↓↓∀x v.(x ε v ≡ ∃u.(u istail v ∧ x = ␈↓αa␈↓↓ u))␈↓.

␈↓ α∧␈↓Now we define an ␈↓↓a-list␈↓ - a familiar Lisp concept.  We have

␈↓ α∧␈↓7)␈↓ αt␈α␈↓↓∀w.(isalist␈αw␈α≡␈α∀x.(x␈αε␈αw␈α⊃␈α¬␈↓αa␈↓↓t␈αx)␈α∧␈α∀u1␈α
u2.(u1␈αistail␈αw␈α∧␈αu2␈αistail␈αw␈α∧␈α␈↓αaa␈↓↓␈αu1␈α=␈α␈↓αaa␈↓↓␈αu2␈α
⊃
␈↓ α∧␈↓↓u1 = u2))␈↓.

␈↓ α∧␈↓Thus␈α∞an␈α
␈↓↓a-list␈↓␈α∞is␈α∞a␈α
list␈α∞of␈α
pairs␈α∞such␈α∞that␈α
no␈α∞S-expression␈α
is␈α∞the␈α∞first␈α
element␈α∞of␈α∞two␈α
different
␈↓ α∧␈↓pairs.␈α⊃ Therefore,␈α⊃a-lists␈α⊃are␈α⊃suitable␈α⊃for␈α⊂representing␈α⊃finite␈α⊃lists␈α⊃of␈α⊃argument-value␈α⊃pairs␈α⊂for
␈↓ α∧␈↓partial functions.

␈↓ α∧␈↓␈↓ αTFinally,␈α
we␈α
need␈α
the␈α
familiar␈α
Lisp␈α
function␈α
␈↓↓assoc␈↓␈α
that␈α
is␈α
used␈α
for␈α
looking␈α
up␈α
atoms␈α
on␈α␈↓↓a-
␈↓ α∧␈↓↓lists␈↓.  Its familiar recursive definition is

␈↓ α∧␈↓8)␈↓ αt ␈↓↓assoc(x,w) ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ w ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ x = ␈↓αaa␈↓↓ w ␈↓αthen␈↓↓ ␈↓αa␈↓↓ w ␈↓αelse␈↓↓ assoc(x,␈↓αd␈↓↓ w)␈↓,

␈↓ α∧␈↓but it can be represented by

␈↓ α∧␈↓9)␈↓ αt ␈↓↓∀w x y.(x.y = assoc(x,w) ≡ ∃w1.(w1 istail w ∧ x.y = ␈↓αa␈↓↓ w1) ∨ assoc(x,w) = ␈↓NIL␈↓↓)␈↓.

␈↓ α∧␈↓␈↓ αTNow let ␈↓↓f␈↓ be an arbitrary recursive program defined by

␈↓ α∧␈↓10)␈↓ αt ␈↓↓f x ← ␈↓	t␈↓↓[f](x)␈↓
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f21


␈↓ α∧␈↓for␈αsome␈αcontinuous␈α
functional␈α␈↓	t␈↓.␈α In␈αorder␈α
to␈αemphasize␈αthe␈αparallel␈α
between␈αa␈αpartial␈αfunction␈α
␈↓↓f␈↓
␈↓ α∧␈↓and an ␈↓↓a-list␈↓ used as a finite approximation, we define

␈↓ α∧␈↓11)␈↓ αt ␈↓	t␈↓↓'(w)(x) = ␈↓	t␈↓↓[λz.␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(z,w) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(z,w)](x)␈↓.

␈↓ α∧␈↓Thus␈α␈↓	t␈↓'␈αis␈αlike␈α␈↓	t␈↓␈αexcept␈α
that␈αwhenever␈α␈↓	t␈↓␈αevaluates␈αits␈αfunctional␈α
argument␈α␈↓↓f␈↓␈αat␈αsome␈αvalue␈α␈↓↓z,␈↓␈α
␈↓	t␈↓'
␈↓ α∧␈↓looks up ␈↓↓z␈↓ on the a-list ␈↓↓w.␈↓

␈↓ α∧␈↓␈↓ αTWith this preparation we can write

␈↓ α∧␈↓12)␈↓ αt␈α␈↓↓∀x␈α(¬∃y␈αw.(x.y␈α=␈α␈↓αa␈↓↓␈αw␈α∧␈α∀x1␈αy1␈αw1.(w1␈αistail␈αw␈α∧␈αx1.y1␈α=␈α␈↓αa␈↓↓␈αw1␈α⊃␈αy1␈α=␈α␈↓	t␈↓↓'[␈↓αd␈↓↓␈αw1](x1)))␈α⊃
␈↓ α∧␈↓↓f(x)␈α=␈α␈↓πT␈↓↓)␈α∧␈α
∀y.(∃w.(x.y␈α=␈α␈↓αa␈↓↓␈αw␈α∧␈α
∀x1␈αy1␈αw1.(w1␈αistail␈αw␈α
∧␈αx1.y1␈α=␈α␈↓αa␈↓↓␈αw1␈α
⊃␈αy1␈α=␈α␈↓	t␈↓↓'[␈↓αd␈↓↓␈α
w1](x1))))␈α⊃
␈↓ α∧␈↓↓f(x) = y))␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α∞essence␈α
of␈α∞this␈α
formula␈α∞is␈α
simple.␈α∞ ␈↓↓w␈↓␈α
is␈α∞an␈α
a-list␈α∞containing␈α
all␈α∞argument-value␈α
pairs
␈↓ α∧␈↓that␈α⊂arise␈α⊂in␈α⊂the␈α⊂evaluation␈α∂of␈α⊂␈↓↓f(x).␈↓␈α⊂We␈α⊂require␈α⊂that␈α⊂if␈α∂␈↓↓x␈↓␈α⊂occurs␈α⊂somewhere␈α⊂on␈α⊂␈↓↓w,␈↓␈α⊂the␈α∂pairs
␈↓ α∧␈↓involved␈α∂in␈α∂the␈α∂evaluation␈α∂of␈α∞␈↓↓f(x)␈↓␈α∂occur␈α∂further␈α∂on␈α∂in␈α∂the␈α∞a-list␈α∂␈↓↓w.␈↓␈α∂This␈α∂is␈α∂to␈α∂avoid␈α∞allowing
␈↓ α∧␈↓circular recursions.  If there is no such a-list, then ␈↓↓f(x) = ␈↓πT␈↓↓.

␈↓ α∧␈↓␈↓ αTIf␈α
the␈αlogic␈α
has␈α
a␈αdescription␈α
operator␈α
␈↓	i␈↓,␈αwhere␈α
␈↓	i␈↓↓␈α
x.P(x)␈↓␈αstands␈α
for␈α
the␈α"the␈α
unique␈α
␈↓↓x␈↓␈αsuch
␈↓ α∧␈↓that ␈↓↓P(x)␈↓ if there is such a unique ␈↓↓x␈↓ and otherwise ␈↓πT␈↓", then (12) can be written

␈↓ α∧␈↓13)␈↓ αt␈α∂␈↓↓∀x.(f(x)␈α∂=␈α∂␈↓	i␈↓↓␈α∂y.∃w.(x.y␈α∂=␈α∂␈↓αa␈↓↓␈α∞w␈α∂∧␈α∂∀x1␈α∂y1␈α∂w1.(w1␈α∂istail␈α∂w␈α∞∧␈α∂x1.y1␈α∂=␈α∂␈↓αa␈↓↓␈α∂w1␈α∂⊃␈α∂y1␈α∂=␈α∞␈↓	t␈↓↓'[␈↓αd␈↓↓
␈↓ α∧␈↓↓w1](x1))))␈↓.

␈↓ α∧␈↓␈↓ αTAs an example, consider the Lisp function ␈↓↓ff␈↓ defined recursively by

␈↓ α∧␈↓14)␈↓ αt ␈↓↓ff x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ ff ␈↓αa␈↓↓ x␈↓.

␈↓ α∧␈↓(13) then takes the form

␈↓ α∧␈↓15)␈↓ αt␈α
∀x.(ff␈αx␈α
=␈α␈↓	i␈↓↓y.∃w.(x.y␈α
=␈α
␈↓αa␈↓↓␈αw␈α
∧␈α∀x1␈α
y1␈α
w1.(w1␈αistail␈α
w␈α∧␈α
x1.y1␈α
=␈α␈↓αa␈↓↓␈α
w1␈α⊃␈α
y1␈α
=␈α␈↓αif␈↓↓␈α
␈↓αa␈↓↓t␈αx1␈α
␈↓αthen␈↓↓
␈↓ α∧␈↓↓x1 ␈↓αelse␈↓↓ (␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(x1,␈↓αd␈↓↓ w1) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(x1,␈↓αd␈↓↓ w1)))))␈↓.

␈↓ α∧␈↓␈↓ αTSuppose␈α∞we␈α∞were␈α∞computing␈α∞␈↓↓ff ((A.B).C)␈↓.␈α
 A␈α∞suitable␈α∞␈↓↓w␈↓␈α∞would␈α∞be␈α∞((((A.B).C).A)␈α
((A.B).A)
␈↓ α∧␈↓(A.A)).

␈↓ α∧␈↓␈↓ αTIt␈α∂might␈α∂be␈α⊂asked␈α∂whether␈α∂␈↓↓occur␈↓␈α∂is␈α⊂necessary.␈α∂ Couldn't␈α∂we␈α∂represent␈α⊂recursive␈α∂programs
␈↓ α∧␈↓using␈αjust␈α␈↓↓car,␈αcdr,␈αcons␈↓␈αand␈α␈↓↓atom␈↓?␈α No,␈αfor␈αthe␈αfollowing␈αreason.␈α Suppose␈αthat␈αthe␈αfunction␈α␈↓↓f␈↓␈αis
␈↓ α∧␈↓representable using only the basic Lisp functions without ␈↓↓subexp␈↓, and consider the sentence

␈↓ α∧␈↓16)␈↓ αt ␈↓↓∀x.issexp f(x)␈↓,

␈↓ α∧␈↓asserting␈αthe␈αtotality␈α
of␈α␈↓↓f.␈↓␈αUsing␈α
the␈αrepresentation,␈αwe␈α
can␈αwrite␈α(16)␈α
as␈αa␈αsentence␈αinvolving␈α
only
␈↓ α∧␈↓the␈α⊂basic␈α⊃Lisp␈α⊂functions␈α⊃and␈α⊂the␈α⊂constant␈α⊃␈↓πT␈↓.␈α⊂ However,␈α⊃may␈α⊂be␈α⊂shown␈α⊃in␈α⊂Appendix␈α⊃I,␈α⊂these
␈↓ α∧␈↓sentences␈αare␈αdecidable,␈αand␈αtotality␈αisn't.␈α (I'll␈αput␈αthe␈αproof␈αin␈αAppendix␈αI␈αif␈αI␈αcan␈αprove␈αit.␈α At
␈↓ α∧␈↓this time, I think I've almost got it).

␈↓ α∧␈↓␈↓ αTIn␈α∞case␈α∞of␈α∞functions␈α∞of␈α∞several␈α∞variables,␈α∞(12)␈α∞corresponds␈α∞to␈α∞a␈α∂call-by-value␈α∞computation
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f22


␈↓ α∧␈↓rule␈αwhile␈αthe␈αrepresentations␈αof␈αthe␈αprevious␈αsections␈αcorrespond␈αto␈αcall-by-name␈αor␈αother␈α"safe"
␈↓ α∧␈↓rules.␈α∞ The␈α∞difference␈α∂is␈α∞not␈α∞important,␈α∂because␈α∞of␈α∞Vuillemin's␈α∂theorem␈α∞that␈α∞any␈α∂strict␈α∞function
␈↓ α∧␈↓may be computed either according to call-by-name or call-by-value.


␈↓ α∧␈↓α12. Questions of Incompleteness.

␈↓ α∧␈↓␈↓ αTLuckham,␈αPark␈αand␈αPaterson␈α(1970)␈αhave␈αshown␈αthat␈αwhether␈αa␈αprogram␈α
schema␈αdiverges
␈↓ α∧␈↓for␈α∞every␈α∞interpretation,␈α∂whether␈α∞it␈α∞diverges␈α∞for␈α∂some␈α∞interpretation,␈α∞and␈α∞whether␈α∂two␈α∞program
␈↓ α∧␈↓schemas␈α∀are␈α∪equivalent␈α∀are␈α∀all␈α∪not␈α∀even␈α∪partially␈α∀solvable␈α∀problems.␈α∪ Manna␈α∀(1974)␈α∀has␈α∪a
␈↓ α∧␈↓thorough␈αdiscussion␈αof␈αthese␈αpoints.␈α In␈αview␈αof␈αthese␈αresults,␈αwhat␈αcan␈αbe␈αexpected␈αfrom␈αour␈αfirst
␈↓ α∧␈↓order representations?

␈↓ α∧␈↓␈↓ αTFirst␈α
let␈α
us␈α
construct␈α
a␈α
Lisp␈α
computation␈α
that␈α
does␈α
not␈α
terminate,␈α
but␈α
whose␈α
non-termination
␈↓ α∧␈↓cannot␈α
be␈α
proved␈α
from␈α
the␈αaxioms␈α
Lisp1␈α
within␈α
first␈α
order␈αlogic.␈α
 We␈α
need␈α
only␈α
program␈αa␈α
proof-
␈↓ α∧␈↓checker␈α
for␈αfirst␈α
order␈α
logic,␈αset␈α
it␈α
to␈αgenerate␈α
all␈αpossible␈α
proofs␈α
starting␈αwith␈α
the␈α
axioms␈αLisp1,
␈↓ α∧␈↓and␈α
stop␈α
when␈α
it␈αfinds␈α
a␈α
proof␈α
of␈α(NIL␈α
≠␈α
NIL)␈α
or␈αsome␈α
other␈α
contradiction.␈α
 Assuming␈αthe␈α
axioms
␈↓ α∧␈↓are␈α
consistent,␈αthe␈α
program␈αwill␈α
never␈α
find␈αsuch␈α
a␈αproof␈α
and␈α
will␈αnever␈α
stop.␈α In␈α
fact,␈αproving␈α
that
␈↓ α∧␈↓the␈α⊂program␈α⊂will␈α⊂never␈α⊂stop␈α⊂is␈α⊃precisely␈α⊂proving␈α⊂that␈α⊂the␈α⊂axioms␈α⊂are␈α⊂consistent.␈α⊃ But␈α⊂G␈↓
:␈↓odel's
␈↓ α∧␈↓theorem␈αasserts␈αthat␈αaxiom␈αsystems␈αlike␈αLisp1␈αcannot␈αbe␈αproved␈αconsistent␈αwithin␈αthemselves.␈α All
␈↓ α∧␈↓the␈αknown␈αcases␈αof␈αterminating␈αcomputations␈αthat␈αcan't␈αbe␈αproved␈αnot␈αto␈αterminate␈αwithin␈αPeano
␈↓ α∧␈↓arithmetic involve such an appeal to G␈↓
:␈↓odel's theorem or similar unsolvability arguments.

␈↓ α∧␈↓␈↓ αTWe␈α
can␈α
presumably␈α
prove␈α
Lisp1␈α
consistent␈α
just␈α
as␈α
Gentzen␈α
proved␈α
arithmetic␈α∞consistent␈α
-
␈↓ α∧␈↓by␈α∩introducing␈α∪a␈α∩new␈α∩axiom␈α∪schema␈α∩that␈α∩allows␈α∪induction␈α∩up␈α∩to␈α∪the␈α∩transfinite␈α∪ordinal␈α∩ε␈↓β0␈↓.
␈↓ α∧␈↓Proving the new system consistent would require induction up to a still higher ordinal, etc.

␈↓ α∧␈↓␈↓ αTSince␈α∞every␈α∞recursively␈α∞defined␈α∞function␈α∞can␈α∞be␈α∞defined␈α∞explicitly,␈α∞any␈α∞sentence␈α
involving
␈↓ α∧␈↓such␈αfunctions␈αcan␈αbe␈αreplaced␈αby␈αan␈αequivalent␈αsentence␈αinvolving␈αonly␈α␈↓↓occur␈↓␈αand␈αthe␈αbasic␈αLisp
␈↓ α∧␈↓functions.␈α The␈αtheory␈αof␈α
␈↓↓occur␈↓␈αand␈αthese␈αfunctions␈αhas␈α
a␈αstandard␈αmodel,␈αthe␈αusual␈α
S-expressions
␈↓ α∧␈↓and␈α∪many␈α∩non-standard␈α∪models.␈α∩ We␈α∪"construct"␈α∩non-standard␈α∪models␈α∩in␈α∪the␈α∩usual␈α∪way␈α∩by
␈↓ α∧␈↓appealing␈α
to␈α
the␈α
theorem␈α
that␈α
if␈α
every␈α
finite␈α
subset␈α
of␈α
a␈α
set␈α
␈↓↓S␈↓␈α
of␈α
sentences␈α
of␈α
first␈α
order␈α
logic␈αhas␈α
a
␈↓ α∧␈↓model,␈αthen␈α␈↓↓S␈↓␈αhas␈αa␈αmodel.␈α For␈αexample,␈αtake␈α␈↓↓S␈α=␈α{occur[␈↓NIL␈↓↓,␈αx],␈αoccur[␈↓(A)␈↓↓,␈αx],␈αoccur[␈↓(A␈αA)␈↓↓␈α,
␈↓ α∧␈↓↓x],␈α...␈↓␈αindefinitely}.␈α Every␈αfinite␈αsubset␈αof␈α␈↓↓S␈↓␈αhas␈αa␈αmodel;␈αwe␈αneed␈αonly␈αtake␈α␈↓↓x␈↓␈αto␈αbe␈αthe␈αlongest
␈↓ α∧␈↓list␈αof␈αA's␈αoccurring␈αin␈αthe␈αsentences.␈α Hence␈αthere␈αis␈αa␈αmodel␈αof␈αthe␈αLisp␈αaxioms␈αin␈αwhich␈α␈↓↓x␈↓␈αhas
␈↓ α∧␈↓all␈α∞lists␈α∂of␈α∞A's␈α∞as␈α∂subexpressions.␈α∞ No␈α∞sentence␈α∂true␈α∞in␈α∞the␈α∂standard␈α∞model␈α∞and␈α∂false␈α∞in␈α∂such␈α∞a
␈↓ α∧␈↓model␈αcan␈αbe␈αproved␈αfrom␈αthe␈αaxioms.␈α However,␈αit␈αis␈αnecessary␈αto␈αbe␈αcareful␈αabout␈αthe␈αmeaning
␈↓ α∧␈↓of␈αtermination␈αof␈αa␈αfunction.␈α
 In␈αfact,␈αtaking␈αsuccessive␈α␈↓↓cdr␈↓s␈α
of␈αsuch␈αan␈α␈↓↓x␈↓␈αwould␈α
never␈αterminate,
␈↓ α∧␈↓but␈α
the␈αsentence␈α
whose␈α␈↓↓standard␈α
interpretation␈↓␈αis␈α
termination␈αof␈α
the␈αcomputation␈α
is␈αprovable␈α
from
␈↓ α∧␈↓Lisp1.

␈↓ α∧␈↓␈↓ αTThe␈α⊂practical␈α⊂question␈α∂is:␈α⊂where␈α⊂does␈α∂the␈α⊂correctness␈α⊂of␈α∂ordinary␈α⊂programs␈α⊂come␈α⊂in?␈α∂ It
␈↓ α∧␈↓seems␈αlikely␈α
that␈αsuch␈α
statements␈αwill␈αbe␈α
provable␈αwith␈α
our␈αoriginal␈αsystem␈α
of␈αaxioms.␈α
 It␈αdoesn't
␈↓ α∧␈↓follow␈α
that␈α
the␈α
system␈α
Lisp1␈α
will␈α∞permit␈α
convenient␈α
proofs,␈α
but␈α
probably␈α
it␈α
will.␈α∞ Some␈α
heuristic
␈↓ α∧␈↓evidence␈α
for␈α
this␈α
comes␈α
from␈α
(Cohen␈α
1965).␈α
 Cohen␈α
presents␈α
two␈α
systems␈α
of␈α
axiomatized␈α
arithmetic
␈↓ α∧␈↓Z1␈α
and␈α
Z2.␈α
 Z1␈α∞is␈α
ordinary␈α
Peano␈α
arithmetic␈α∞with␈α
an␈α
axiom␈α
schema␈α∞of␈α
induction,␈α
and␈α
Z2␈α∞is␈α
an
␈↓ α∧␈↓axiomatization␈α
of␈αhereditarily␈α
finite␈α
sets␈αof␈α
integers.␈α Superficially,␈α
Z2␈α
is␈αmore␈α
powerful␈α
than␈αZ1,
␈↓ α∧␈↓but␈αbecause␈αthe␈αset␈αoperations␈αof␈αZ2␈αcan␈αbe␈αrepresented␈αin␈αZ1␈αas␈αfunctions␈αon␈αthe␈αG␈↓
:␈↓odel␈αnumbers
␈↓ α∧␈↓of␈α⊃the␈α⊃sets,␈α∩it␈α⊃turns␈α⊃out␈α∩that␈α⊃Z1␈α⊃is␈α⊃just␈α∩as␈α⊃powerful␈α⊃once␈α∩the␈α⊃necessary␈α⊃machinery␈α∩has␈α⊃been
␈↓ α∧␈↓REPRESENTATION␈↓ ¬YCartwright and McCarthy␈↓ f23


␈↓ α∧␈↓established.␈α Because␈αsets␈αand␈αlists␈αare␈αthe␈αbasic␈αdata␈αof␈αLisp1,␈αand␈αsets␈αare␈αeasily␈αrepresented,␈αthe
␈↓ α∧␈↓power␈αof␈αLisp1␈αwill␈αbe␈αapproximately␈αthat␈αof␈αZ2,␈αand␈αconvenient␈αproofs␈αof␈αcorrectness␈αstatements
␈↓ α∧␈↓should␈α
be␈αpossible.␈α
 Moreover,␈α
since␈αLisp1␈α
is␈αa␈α
first␈α
order␈αtheory,␈α
it␈α
is␈αeasily␈α
extended␈αwith␈α
axioms
␈↓ α∧␈↓for␈α
sets,␈αand␈α
this␈α
should␈αhelp␈α
make␈α
informal␈αproofs␈α
easy␈αto␈α
express.␈α
 It␈αwould␈α
be␈α
nice␈αto␈α
be␈αable␈α
to
␈↓ α∧␈↓express these considerations less vaguely.


␈↓ α∧␈↓α13. References.

␈↓ α∧␈↓␈↓αCartwright,␈αR.S.␈α(1977)␈↓:␈α
␈↓↓A␈αPractical␈αFormal␈α
Semantic␈αDefinition␈αand␈α
Verification␈αSystem␈αfor␈α
Typed
␈↓ α∧␈↓↓Lisp␈↓, Ph.D. Thesis, Computer Science Department, Stanford University, Stanford, California.

␈↓ α∧␈↓␈↓αCohen, Paul (1966)␈↓: ␈↓↓Set Theory and the Continuum Hypothesis␈↓, W.A. Benjamin Inc.

␈↓ α∧␈↓␈↓αCooper,␈αD.C.␈α(1969)␈↓:␈α"Program␈αScheme␈αEquivalences␈αand␈αSecond-order␈αLogic",␈αin␈αB.␈αMeltzer␈αand
␈↓ α∧␈↓D. Michie (eds.), ␈↓↓Machine Intelligence␈↓, Vol. 4, pp. 3-15, Edinburgh University Press, Edinburgh.

␈↓ α∧␈↓␈↓αKleene, S.C. (1951)␈↓: ␈↓↓Introduction to Metamathematics␈↓, Van Nostrand, New York.

␈↓ α∧␈↓␈↓αLuckham,␈αD.C.,␈αD.M.R.Park,␈α
and␈αM.S.␈αPaterson␈α(1970)␈↓:␈α
"On␈αFormalized␈αComputer␈αPrograms",␈α
␈↓↓J.
␈↓ α∧␈↓↓CSS␈↓, ␈↓α4␈↓(3): 220-249 (June).

␈↓ α∧␈↓␈↓αManna,␈αZohar␈αand␈α
Amir␈αPnueli␈α(1970)␈↓:␈α
"Formalization␈αof␈αthe␈α
Properties␈αof␈αFunctional␈α
Programs",
␈↓ α∧␈↓␈↓↓J. ACM␈↓, ␈↓α17␈↓(3): 555-569.

␈↓ α∧␈↓␈↓αManna, Zohar (1974)␈↓: ␈↓↓Mathematical Theory of Computation␈↓, McGraw-Hill.

␈↓ α∧␈↓␈↓αManna,␈α∀Zohar,␈α∀Stephen␈α∀Ness␈α∀and␈α∀Jean␈α∀Vuillemin␈α∀(1973)␈↓:␈α∀"Inductive␈α∀Methods␈α∀for␈α∀Proving
␈↓ α∧␈↓Properties of Programs", ␈↓↓Comm. ACM␈↓,␈↓α16␈↓(8): 491-502 (August).

␈↓ α∧␈↓␈↓αMcCarthy,␈αJohn␈↓␈α(1963)␈α"A␈α
Basis␈αfor␈αa␈αMathematical␈αTheory␈α
of␈αComputation",␈αin␈αP.␈αBraffort␈α
and
␈↓ α∧␈↓D.␈α⊃Hirschberg␈α⊃(eds.),␈α⊂␈↓↓Computer␈α⊃Programming␈α⊃and␈α⊂Formal␈α⊃Systems␈↓,␈α⊃pp.␈α⊃33-70.␈α⊂ North-Holland
␈↓ α∧␈↓Publishing Company, Amsterdam.

␈↓ α∧␈↓␈↓αMorris,␈α
James␈αH.,␈α
and␈αBen␈α
Wegbreit␈α
(1977)␈↓:␈α"Program␈α
Verification␈αby␈α
Subgoal␈αInduction",␈α
␈↓↓Comm.
␈↓ α∧␈↓↓ACM␈↓,␈↓α20␈↓(4): 209-222 (April).

␈↓ α∧␈↓␈↓αPark,␈α_David␈α_(1969)␈↓:␈α_Fixpoint␈α_Induction␈α_and␈α_Proofs␈α_of␈α_Program␈α_Properties",␈α_in␈α↔␈↓↓Machine
␈↓ α∧␈↓↓Intelligence 5␈↓, pp. 59-78, Edinburgh University Press, Edinburgh.